# Variants of `haveI`/`letI` for use in do-notation. #

This file implements the `haveI'` and `letI'` macros which have the same semantics as `haveI` and `letI`, but are `doElem`s and can be used inside do-notation.

They need an apostrophe after their name for disambiguation with the term variants. This is necessary because the do-notation has a hardcoded list of keywords which can appear both as term-mode and do-elem syntax (like for example `let` or `have`).

source
def Mathlib.Tactic.HaveI.doElemHaveI'_ :
Lean.ParserDescr

`haveI'` behaves like `have`, but inlines the value instead of producing a `have` term.

(This is the do-notation version of the term-mode `haveI`.)

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.HaveI.doElemLetI'_ :
Lean.ParserDescr

`letI` behaves like `let`, but inlines the value instead of producing a `let` term.

(This is the do-notation version of the term-mode `haveI`.)

Equations

- One or more equations did not get rendered due to their size.

Instances For