knuckledragger
kdrag
Calc
Inductive()
Lemma
NewType()
Proof
QExists()
QForAll()
Record()
axiom()
cond()
define()
lemma()
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.list
kdrag.theories.datatypes.nat
kdrag.theories.datatypes.option
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.option
View page source
kdrag.theories.datatypes.option