@@ -17,6 +17,7 @@ getWitness (a ** v) = a
1717getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)
1818getProof (a ** v) = v
1919
20+||| The eliminator for the empty type.
2021FalseElim : _|_ -> a
2122
2223||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
@@ -43,17 +44,35 @@ lazy x = x -- compiled specially
4344force : a -> a
4445force x = x -- compiled specially
4546
47+||| There are two types of laziness: that arising from lazy functions, and that
48+||| arising from codata. They differ in their totality condition.
4649data LazyType = LazyCodata | LazyEval
4750
51+||| The underlying implementation of Lazy and Inf.
4852data Lazy' : LazyType -> Type -> Type where
53+ ||| A delayed computation.
54+ |||
55+ |||Delay is inserted automatically by the elaborator where necessary.
56+ |||
57+ ||| Note that compiled code gives `Delay` special semantics.
58+ ||| @ t whether this is laziness from codata or normal lazy evaluation
59+ ||| @ a the type of the eventual value
60+ ||| @ val a computation that will produce a value
4961 Delay : {t, a : _} -> (val : a) -> Lazy' t a
5062
63+||| Compute a value from a delayed computation.
64+|||
65+||| Inserted by the elaborator where necessary.
5166Force : {t, a : _} -> Lazy' t a -> a
5267Force (Delay x) = x
5368
69+||| Lazily evaluated values. This has special evaluation semantics.
5470Lazy : Type -> Type
5571Lazy t = Lazy' LazyEval t
5672
73+||| Recursive parameters to codata. Inserted automatically by the elaborator
74+||| on a "codata" definition but is necessary by hand if mixing inductive and
75+||| coinductive parameters.
5776Inf : Type -> Type
5877Inf t = Lazy' LazyCodata t
5978