Add FalseElim as a primitive
commit9a59cb5a6fdf0767e3f93a57e6e3bc03da24596d
authorEdwin Brady <eb@cs.st-andrews.ac.uk>
dateThu 17 Nov 2011, 16:20 (15 years ago)
parentda5e25e
lib/builtins.idr+2
@@ -7,6 +7,8 @@ getSigIdx (Exists a v) = a;
77getSigVal : {P : a -> Set} -> (s : Sigma a P) -> P (getSigIdx s);
88getSigVal (Exists a v) = v;
99
10+FalseElim : _|_ -> a;
11+
1012-- For rewrite tactic
1113replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Set} -> x = y -> P x -> P y;
1214replace refl prf = prf;
src/Idris/Compiler.hs+1−1
@@ -13,7 +13,7 @@ import Control.Monad.State
1313import Epic.Epic hiding (Term, Type, Name, fn, compile)
1414import qualified Epic.Epic as E
1515
16−primDefs = [UN ["mkForeign"]]
16+primDefs = [UN ["mkForeign"], UN ["FalseElim"]]
1717
1818compile :: FilePath -> Idris ()
1919compile f = do ds <- mkDecls