Partial values of a type #
This file defines
part α, the partial values of a type.
o : part α carries a proposition
o.dom, its domain, along with a function
get : o.dom → α, its
value. The rule is then that every partial value has a value but, to access it, you need to provide
a proof of the domain.
part α behaves the same as
option α except that
o : option α is decidably
a : α, while the domain of
o : part α doesn't have to be decidable. That means you can
translate back and forth between a partial value with a decidable domain and an option, and
option α and
part α are classically equivalent. In general,
part α is bigger than
Main declarations #
part.none: The partial value whose domain is
part.some a: The partial value whose domain is
trueand whose value is
part.of_option: Converts an
option αto a
part αby sending
part.to_option: Converts a
part αwith a decidable domain to an
part.equiv_option: Classical equivalence between
o.bind fhas value
(f (o.get _)).get _(
f omorally) and is defined when
f (o.get _)are defined.
part.map: Maps the value and keeps the same domain.
part.restrict p oreplaces the domain of
o : part αby
p : Propso long as
p → o.dom.
assert p fappends
pto the domains of the values of a partial function.
part.unwrap: Gets the value of a partial value regardless of its domain. Unsound.
a : α,
o : part α,
a ∈ o means that
o is defined and equal to
a. Formally, it means
o.get _ = a.
part α the order where everything is greater than