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.
theorem
semiquot.eq_mk_of_mem
{α : Type u_1}
{q : semiquot α}
{a : α}
(h : a ∈ q) :
q = semiquot.mk h
pure a is a reinterpreted as an unspecified element of {a}.
Equations
Replace s in a q : semiquot α with a union s ∪ q.s
Equations
- semiquot.blur s q = q.blur' _
theorem
semiquot.blur_eq_blur'
{α : Type u_1}
(q : semiquot α)
(s : set α)
(h : q.s ⊆ s) :
semiquot.blur s q = q.blur' h
@[simp]
@[simp]
@[instance]
Equations
- semiquot.is_lawful_monad = _
- _ = _
- _ = _
@[instance]
Equations
- semiquot.partial_order = {le := λ (s t : semiquot α), ∀ ⦃x : α⦄, x ∈ s → x ∈ t, lt := preorder.lt._default (λ (s t : semiquot α), ∀ ⦃x : α⦄, x ∈ s → x ∈ t), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
@[instance]
Equations
- semiquot.semilattice_sup = {sup := λ (s : semiquot α), semiquot.blur s.s, le := partial_order.le semiquot.partial_order, lt := partial_order.lt semiquot.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}
@[simp]
theorem
semiquot.eq_pure
{α : Type u_1}
{q : semiquot α}
(p : q.is_pure) :
q = has_pure.pure (q.get p)
theorem
semiquot.is_pure_iff
{α : Type u_1}
{s : semiquot α} :
s.is_pure ↔ ∃ (a : α), s = has_pure.pure a
theorem
semiquot.is_pure_of_subsingleton
{α : Type u_1}
[subsingleton α]
(q : semiquot α) :
q.is_pure
univ : semiquot α represents an unspecified element of univ : set α.
Equations
- semiquot.univ = semiquot.mk semiquot.univ._proof_1
@[instance]
Equations
- semiquot.inhabited = {default := semiquot.univ _inst_1}
@[simp]
@[instance]
Equations
- semiquot.order_top = {top := semiquot.univ _inst_1, le := partial_order.le semiquot.partial_order, lt := partial_order.lt semiquot.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}
@[instance]
Equations
- semiquot.semilattice_sup_top = {top := order_top.top semiquot.order_top, le := order_top.le semiquot.order_top, lt := order_top.lt semiquot.order_top, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, sup := semilattice_sup.sup semiquot.semilattice_sup, le_sup_left := _, le_sup_right := _, sup_le := _}