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} (tac : tactic α) :

tactic α

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

source

meta def tactic.unfreezing_hyp (h : expr) (tac : 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 (tac : 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.revertI (ids : interactive.parse (lean.parser.many lean.parser.ident)) :

tactic unit

Like revert, but can also revert instance arguments.

source

meta def tactic.interactive.substI (q : interactive.parse interactive.types.texpr) :

tactic unit

Like subst, but can also substitute in instance arguments.

source

meta def tactic.interactive.casesI (p : interactive.parse tactic.interactive.cases_arg_p) (q : 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 (p : interactive.parse (optional interactive.types.ident_)) :

tactic unit

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

source

meta def tactic.interactive.introsI (p : 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 (h : interactive.parse (optional lean.parser.ident)) (q₁ : interactive.parse (optional (lean.parser.tk ":" *> interactive.types.texpr))) (q₂ : interactive.parse (optional (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.

source

meta def tactic.interactive.letI (h : interactive.parse (optional lean.parser.ident)) (q₁ : interactive.parse (optional (lean.parser.tk ":" *> interactive.types.texpr))) (q₂ : interactive.parse (optional (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 let.

source

meta def tactic.interactive.exactI (q : interactive.parse interactive.types.texpr) :

tactic unit

Like exact, but uses all variables in the context for typeclass inference.