git.iko.soy/Idris-dev
on master help sign in
Define void with an elab script, not elim_for
f4bfe5cShea Levy
libs/prelude/Builtins.idr−1
compare with master
unifiedsplit
@@ -48,7 +48,6 @@ namespace Builtins
48
48
49||| The eliminator for the `Void` type.
49||| The eliminator for the `Void` type.
50void : Void -> a
50void : Void -> a
51−void {a} v = elim_for Void (\_ => a) v
52
51
53||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
52||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
54data Symbol_ : String -> Type where
53data Symbol_ : String -> Type where
libs/prelude/Prelude.idr+2
@@ -37,6 +37,8 @@ import public Language.Reflection.Errors
37%default total
37%default total
38
38
39-- Things that can't be elsewhere for import cycle reasons
39-- Things that can't be elsewhere for import cycle reasons
40+%runElab (defineFunction $ DefineFun `{void} [])
41+
40decAsBool : Dec p -> Bool
42decAsBool : Dec p -> Bool
41decAsBool (Yes _) = True
43decAsBool (Yes _) = True
42decAsBool (No _) = False
44decAsBool (No _) = False