@@ -130,14 +130,14 @@ data Delayed : DelayReason -> Type -> Type where
130Force : {t, a : _} -> Delayed t a -> a
130Force : {t, a : _} -> Delayed t a -> a
131Force (Delay x) = x
131Force (Delay x) = x
133−||| Lazily evaluated values.
133+||| Lazily evaluated values.
134||| At run time, the delayed value will only be computed when required by
134||| At run time, the delayed value will only be computed when required by
135||| a case split.
135||| a case split.
136%error_reverse
136%error_reverse
137Lazy : Type -> Type
137Lazy : Type -> Type
138Lazy t = Delayed LazyValue t
138Lazy t = Delayed LazyValue t
140−||| Possibly infinite data.
140+||| Possibly infinite data.
141||| A value which may be infinite is accepted by the totality checker if
141||| A value which may be infinite is accepted by the totality checker if
142||| it appears under a data constructor. At run time, the delayed value will
142||| it appears under a data constructor. At run time, the delayed value will
143||| only be computed when required by a case split.
143||| only be computed when required by a case split.
@@ -187,22 +187,16 @@ idris_crash : (msg : String) -> a
188||| Subvert the type checker. This function is abstract, so it will not reduce in
188||| Subvert the type checker. This function is abstract, so it will not reduce in
189||| the type checker. Use it with care - it can result in segfaults or worse!
189||| the type checker. Use it with care - it can result in segfaults or worse!
191believe_me : a -> b
191believe_me : a -> b
192believe_me x = assert_total (prim__believe_me _ _ x)
192believe_me x = assert_total (prim__believe_me _ _ x)
194||| Subvert the type checker. This function *will* reduce in the type checker.
194||| Subvert the type checker. This function *will* reduce in the type checker.
195||| Use it with extreme care - it can result in segfaults or worse!
195||| Use it with extreme care - it can result in segfaults or worse!
196−public export
196+public export
197really_believe_me : a -> b
197really_believe_me : a -> b
198really_believe_me x = assert_total (prim__believe_me _ _ x)
198really_believe_me x = assert_total (prim__believe_me _ _ x)
200−||| Deprecated alias for `Double`, for the purpose of backwards
201−||| compatibility. Idris does not support 32 bit floats at present.
206-- Pointers as external primitive; there's no literals for these, so no
200-- Pointers as external primitive; there's no literals for these, so no
207-- need for them to be part of the compiler.
201-- need for them to be part of the compiler.