kdrag.notation.Inductive

kdrag.notation.Inductive(name: str, strict=True) → DatatypeSortRef

Declare datatypes with auto generated induction principles. Wrapper around z3.Datatype