knuckledragger
kdrag
kdrag.all
kdrag.config
kdrag.kernel
kdrag.notation
kdrag.smt
kdrag.solvers
kdrag.tactics
kdrag.theories
kdrag.theories.bitvec
kdrag.theories.complex
kdrag.theories.datatypes
kdrag.theories.datatypes.induct
kdrag.theories.datatypes.nat
kdrag.theories.int
kdrag.theories.interval
kdrag.theories.real
kdrag.theories.seq
kdrag.theories.vec
kdrag.utils
knuckledragger
kdrag
kdrag.theories
kdrag.theories.datatypes
kdrag.theories.datatypes.induct
View page source
kdrag.theories.datatypes.induct
kdrag.theories.datatypes.
induct
(
DT
:
DatatypeSortRef
)
→
None
Build a basic induction principle for an algebraic datatype