Defines variants of have and let syntax which do not produce let_fun or let bindings, but instead inline the value instead.

This is useful to declare local instances and proofs in theorem statements and subgoals, where the extra binding is inconvenient.

ink

def Std.Tactic.haveI : Lean.Parser.Parser

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

Equations

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

ink

def Std.Tactic.letI : Lean.Parser.Parser

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

Equations

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

ink

def Std.Tactic.tacticHaveI_ : Lean.ParserDescr

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

Equations

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

ink

def Std.Tactic.tacticLetI_ : Lean.ParserDescr

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

Equations

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