Reset the instance cache for the main goal.

Unfreeze local instances, which allows us to revert instances in the context.

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

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

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

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>.

Used to add typeclasses to the context so that they can be used in typeclass inference. The syntax is the same as let.

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