Induction_arg

Ltac2.Syntax.Induction_arg

type t

• see Reference manual, induction_arg

val on_constr : constr_with_bindings -> t

on_constr t performs induction/case analysis on t.

val on_hyp : hypothesis -> t

on_hyp h performs induction/case analysis on hypothesis h.