git.iko.soy/Idris-dev
on master help sign in
Add FalseElim as a primitive
9a59cb5Edwin Brady
lib/builtins.idr+2
compare with master
unifiedsplit
@@ -7,6 +7,8 @@ getSigIdx (Exists a v) = a;
7getSigVal : {P : a -> Set} -> (s : Sigma a P) -> P (getSigIdx s);
7getSigVal : {P : a -> Set} -> (s : Sigma a P) -> P (getSigIdx s);
8getSigVal (Exists a v) = v;
8getSigVal (Exists a v) = v;
9
9
10+FalseElim : _|_ -> a;
11+
10-- For rewrite tactic
12-- For rewrite tactic
11replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Set} -> x = y -> P x -> P y;
13replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Set} -> x = y -> P x -> P y;
12replace refl prf = prf;
14replace refl prf = prf;
src/Idris/Compiler.hs+1−1
@@ -13,7 +13,7 @@ import Control.Monad.State
13import Epic.Epic hiding (Term, Type, Name, fn, compile)
13import Epic.Epic hiding (Term, Type, Name, fn, compile)
14import qualified Epic.Epic as E
14import qualified Epic.Epic as E
15
15
16−primDefs = [UN ["mkForeign"]]
16+primDefs = [UN ["mkForeign"], UN ["FalseElim"]]
17
17
18compile :: FilePath -> Idris ()
18compile :: FilePath -> Idris ()
19compile f = do ds <- mkDecls
19compile f = do ds <- mkDecls