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

This files implements the haveI' and letI' macros which have the same semantics as haveI and letI, but are doElems 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).

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

haveI' behaves like have, but inlines the value instead of producing a let_fun 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.

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

letI behaves like let, but inlines the value instead of producing a let_fun 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.