Semiquotients #
A data type for semiquotients, which are classically equivalent to
nonempty sets, but are useful for programming; the idea is that
a semiquotient set S
represents some (particular but unknown)
element of S
. This can be used to model nondeterministic functions,
which return something in a range of values (represented by the
predicate S
) but are not completely determined.
- mk' :: (
- )
A member of Semiquot α
is classically a nonempty Set α
,
and in the VM is represented by an element of α
; the relation
between these is that the VM element is required to be a member
of the set s
. The specific element of s
that the VM computes
is hidden by a quotient construction, allowing for the representation
of nondeterministic functions.
Instances For
pure a
is a
reinterpreted as an unspecified element of {a}
.
Equations
- Semiquot.pure a = Semiquot.mk (_ : a ∈ {a})
If f
is a constant on q.s
, then q.liftOn f
is the value of f
at any point of q
.
Equations
- Semiquot.liftOn q f h = Trunc.liftOn q.val (fun x => f ↑x) (_ : ∀ (x y : ↑q.s), f ↑x = f ↑y)
Equations
- Semiquot.instMonadSemiquot = Monad.mk
Equations
- One or more equations did not get rendered due to their size.
Extract the value from a IsPure
semiquotient.
Equations
- Semiquot.get q h = Semiquot.liftOn q id h