git.iko.soy/Idris-dev
on master help sign in
Explain the separation between the declaration and definition of void
5ef4a6cShea Levy
libs/prelude/Builtins.idr+6
compare with master
unifiedsplit
@@ -48,6 +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+-- 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
51
57
52||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
58||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
53data Symbol_ : String -> Type where
59data 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+-- See comment after declaration of void in Builtins.idr
41+-- for explanation of this definition's location
40%runElab (defineFunction $ DefineFun `{void} [])
42%runElab (defineFunction $ DefineFun `{void} [])
41
43
42decAsBool : Dec p -> Bool
44decAsBool : Dec p -> Bool