git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2765 from shlevy/no-elim_for

Define void with an elab script, not elim_for

commit180bac56a0436bacd9678f2f77608d542e3fc451 authorDavid Christiansen <david@davidchristiansen.dk> dateFri 27 Nov 2015, 18:08 (11 years ago) parentda709235ef4a6c
2 files changed+10−1
compare with master
unifiedsplit
libs/prelude/Builtins.idr+6−1 libs/prelude/Prelude.idr+4
libs/prelude/Builtins.idr+6−1
@@ -48,7 +48,12 @@ namespace Builtins
4848
4949||| The eliminator for the `Void` type.
5050void : 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
5257
5358||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
5459data Symbol_ : String -> Type where
libs/prelude/Prelude.idr+4
@@ -37,6 +37,10 @@ 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
42+%runElab (defineFunction $ DefineFun `{void} [])
43+
4044decAsBool : Dec p -> Bool
4145decAsBool (Yes _) = True
4246decAsBool (No _) = False