@@ -130,14 +130,14 @@ data Delayed : DelayReason -> Type -> Type where
130130Force : {t, a : _} -> Delayed t a -> a
131131Force (Delay x) = x
132132
133−||| Lazily evaluated values.
133+||| Lazily evaluated values.
134134||| At run time, the delayed value will only be computed when required by
135135||| a case split.
136136%error_reverse
137137Lazy : Type -> Type
138138Lazy t = Delayed LazyValue t
139139
140−||| Possibly infinite data.
140+||| Possibly infinite data.
141141||| A value which may be infinite is accepted by the totality checker if
142142||| it appears under a data constructor. At run time, the delayed value will
143143||| only be computed when required by a case split.
@@ -187,22 +187,16 @@ idris_crash : (msg : String) -> a
187187
188188||| Subvert the type checker. This function is abstract, so it will not reduce in
189189||| the type checker. Use it with care - it can result in segfaults or worse!
190−export
190+export
191191believe_me : a -> b
192192believe_me x = assert_total (prim__believe_me _ _ x)
193193
194194||| Subvert the type checker. This function *will* reduce in the type checker.
195195||| Use it with extreme care - it can result in segfaults or worse!
196−public export
196+public export
197197really_believe_me : a -> b
198198really_believe_me x = assert_total (prim__believe_me _ _ x)
199199
200−||| Deprecated alias for `Double`, for the purpose of backwards
201−||| compatibility. Idris does not support 32 bit floats at present.
202−Float : Type
203−Float = Double
204−%deprecate Float
205−
206200-- Pointers as external primitive; there's no literals for these, so no
207201-- need for them to be part of the compiler.
208202