scilib documentation

core / init.meta.constructor_tactic

source
meta def tactic.get_constructors_for (e : expr) :
tactic (list name)
source
meta def tactic.constructor (cfg : tactic.apply_cfg := {md := tactic.transparency.semireducible, approx := bool.tt, new_goals := tactic.new_goals.non_dep_first, instances := bool.tt, auto_param := bool.tt, opt_param := bool.tt, unify := bool.tt}) :
tactic (list (name × expr))
source
meta def tactic.econstructor  :
tactic (list (name × expr))
source
meta def tactic.fconstructor  :
tactic (list (name × expr))
source
meta def tactic.left  :
tactic (list (name × expr))
source
meta def tactic.right  :
tactic (list (name × expr))
source
meta def tactic.constructor_idx (idx : ℕ) :
tactic (list (name × expr))
source
meta def tactic.split  :
tactic (list (name × expr))
source
meta def tactic.existsi (e : expr) :
tactic unit