mathlib documentation

tactic.pi_instances

pi_instance #

Automation for creating instances of mathematical structures for pi types

source
meta def tactic.pi_instance_derive_field  :
tactic unit

Attempt to clear a goal obtained by refining a pi_instance goal.

source
meta def tactic.pi_instance  :
tactic unit

pi_instance constructs an instance of my_class (Π i : I, f i) where we know Π i, my_class (f i). If an order relation is required, it defaults to pi.partial_order. Any field of the instance that pi_instance cannot construct is left untouched and generated as a new goal.

source
meta def tactic.interactive.pi_instance  :
tactic unit

pi_instance constructs an instance of my_class (Π i : I, f i) where we know Π i, my_class (f i). If an order relation is required, it defaults to pi.partial_order. Any field of the instance that pi_instance cannot construct is left untouched and generated as a new goal.