knuckledragger
kdrag
kdrag.all
kdrag.config
kdrag.kernel
kdrag.notation
kdrag.notation.ExistsUnique
ExistsUnique()
kdrag.notation.NewType
kdrag.notation.QExists
kdrag.notation.QForAll
kdrag.notation.Record
kdrag.notation.cond
kdrag.notation.datatype_call
kdrag.smt
kdrag.solvers
kdrag.tactics
kdrag.theories
kdrag.utils
knuckledragger
kdrag
kdrag.notation
kdrag.notation.ExistsUnique
View page source
kdrag.notation.ExistsUnique
kdrag.notation.
ExistsUnique
(
v
:
ExprRef
,
*
concs
)
→
BoolRef
Unique Existence