Instance cache tactics

For performance reasons, Lean does not automatically update its database of class instances during a proof. The group of tactics in this file helps to force such updates.

source

meta def tactic.reset_instance_cache :

tactic unit

Reset the instance cache for the main goal.

source

meta def tactic.unfreezing {α : Type} :

tactic α → tactic α

Unfreeze the local instances while executing tac on the main goal.

source

meta def tactic.unfreezing_hyp :

expr → tactic unit → tactic unit

Unfreeze local instances while executing tac, if the passed expression is amongst the frozen instances.

source

meta def tactic.interactive.unfreezingI :

tactic.interactive.itactic → tactic unit

unfreezingI { tac } executes tac while temporarily unfreezing the instance cache.

source

meta def tactic.interactive.resetI :

tactic unit

Reset the instance cache. This allows any new instances added to the context to be used in typeclass inference.

source

meta def tactic.interactive.substI :

interactive.parse interactive.types.texpr → tactic unit

Like subst, but can also substitute in instance arguments.

source

meta def tactic.interactive.casesI :

interactive.parse tactic.interactive.cases_arg_p → interactive.parse interactive.types.with_ident_list → tactic unit

Like cases, but can also be used with instance arguments.

source

meta def tactic.interactive.introI :

interactive.parse (optional interactive.types.ident_) → tactic unit

Like intro, but uses the introduced variable in typeclass inference.

source

meta def tactic.interactive.introsI :

interactive.parse (lean.parser.many interactive.types.ident_) → tactic unit

Like intros, but uses the introduced variable(s) in typeclass inference.

source

meta def tactic.interactive.haveI :

interactive.parse (optional lean.parser.ident) → interactive.parse (optional (lean.parser.tk ":" *> interactive.types.texpr)) → interactive.parse (lean.parser.tk ":=" *> interactive.types.texpr) → tactic unit

Used to add typeclasses to the context so that they can be used in typeclass inference. The syntax is the same as have, but the proof-omitted version is not supported. For this one must write have : t, { <proof> }, resetI, <proof>.

source

meta def tactic.interactive.letI :