Documentation

Std.Tactic.HaveI

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.

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.

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.

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.

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.