`Induction_clause`#

Ltac2.Syntax.Induction_clause

type t

val on_constr :
  ?as_pattern:or_and intropattern ->
  ?eqn:naming intropattern ->
  ?where:clause ->
  constr_with_bindings ->
  t

on_constr t ?as_pattern ?eqn ?where builds an induction clause that performs induction on t.

val on_hyp :
  ?as_pattern:or_and intropattern ->
  ?eqn:naming intropattern ->
  ?where:clause ->
  hypothesis ->
  t

on_hyp h ?as_pattern ?eqn ?where builds an induction clause that performs induction on hypothesis h.

Induction_clause#