git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2765 from shlevy/no-elim_for
180bac5David Christiansen
libs/prelude/Builtins.idr+6−1
compare with master
unifiedsplit
@@ -48,7 +48,12 @@ 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
51+-- We can't define void yet. We can't define a function with no clauses without
52+-- elaborator reflection, and we can't do elaborator reflection without
53+-- Language.Reflection.Elab, and Language.Reflection.Elab depends on Builtins.
54+-- We can't delay the declaration of void, because Prelude.Uninhabited depends on
55+-- it, Prelude.Nat depends on Prelude.Uninhabited, and Language.Reflection.Elab
56+-- depends on Prelude.Nat. Instead, void is defined in Prelude.idr
52
57
53||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
58||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
54data Symbol_ : String -> Type where
59data Symbol_ : String -> Type where
libs/prelude/Prelude.idr+4
@@ -37,6 +37,10 @@ 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+-- See comment after declaration of void in Builtins.idr
41+-- for explanation of this definition's location
42+%runElab (defineFunction $ DefineFun `{void} [])
43+
40decAsBool : Dec p -> Bool
44decAsBool : Dec p -> Bool
41decAsBool (Yes _) = True
45decAsBool (Yes _) = True
42decAsBool (No _) = False
46decAsBool (No _) = False