class Void: Any := -- no constructor
class Unit: Any := (): Unit
class Bool: Any :=
true
false
class Reflect (A: Prop): Bool -> Any := -- NEEDED?
true: A -> Reflect true
false: Not A -> Reflect false
class (,) (A B: Any): Any := -- own module 'tuple' ?
(,): A -> B -> (,)
class Result (A B: Any): Any :=
ok : A -> Result
error : B -> Result
class Either (A B: Any): Any :=
left : A -> Either
right : B -> Either
class Decision (A: Prop): Any :=
true: A -> Decision
false: Not A -> Decision
class Maybe (A: Any): Any :=
nothing : Maybe
just : A -> Maybe
class Refine {A: Any} (P: Predicate A) :=
refine x: P x -> Refine
(|>)
{A: Any}
{F: A -> Any}
(x: A)
(f: ∀ x: F x)
: F x
-- 'x |> f': Apply the function 'f' to the argument 'x'.
:=
f x
(<|)
{A: Any}
{F: A -> Any}
(f: ∀ x: F x)
(x: A)
: F x
-- 'f <| x': Apply the function 'f' to the argument 'x'.
:=
f x
(>>)
{A B C: Any}
(f: A -> B)
(g: B -> C)
: A -> C
-- 'f >> g': Apply 'f' and then 'g'.
:=
λ x := g (f x)
(<<)
{A B C: Any}
(g: B -> C)
(f: A -> B)
: A -> C
-- ' g << f': Apply 'f' and then 'g'.
:=
λ x := g (f x)