git.iko.soy/Idris-dev
on master help sign in
Explain the separation between the declaration and definition of void
commit5ef4a6cd6c8b69d74aa622e482f1485f31a036bf authorShea Levy <shea@shealevy.com> dateFri 30 Oct 2015, 07:15 (11 years ago) parentf4bfe5c
2 files changed+8
compare with master
unifiedsplit
libs/prelude/Builtins.idr+6 libs/prelude/Prelude.idr+2
libs/prelude/Builtins.idr+6
@@ -48,6 +48,12 @@ namespace Builtins
4848
4949||| The eliminator for the `Void` type.
5050void : 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
5157
5258||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
5359data Symbol_ : String -> Type where
libs/prelude/Prelude.idr+2
@@ -37,6 +37,8 @@ import public Language.Reflection.Errors
3737%default total
3838
3939-- 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
4042%runElab (defineFunction $ DefineFun `{void} [])
4143
4244decAsBool : Dec p -> Bool