Define void with an elab script, not elim_for
commitf4bfe5c8a794c34b9f7994e1b29ec1fab0d1f5fa
authorShea Levy <shea@shealevy.com>
dateSun 25 Oct 2015, 09:47 (11 years ago)
parent467490b
libs/prelude/Builtins.idr−1
@@ -48,7 +48,6 @@ namespace Builtins
4848
4949||| The eliminator for the `Void` type.
5050void : Void -> a
51−void {a} v = elim_for Void (\_ => a) v
5251
5352||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
5453data 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+%runElab (defineFunction $ DefineFun `{void} [])
41+
4042decAsBool : Dec p -> Bool
4143decAsBool (Yes _) = True
4244decAsBool (No _) = False