kdrag.notation.induct_inductive

kdrag.notation.induct_inductive(DT: DatatypeSortRef, x=None, P=None) → None

Build a basic induction principle for an algebraic datatype