added if0Nat to the SAWCore Prelude

GaloisInc · May 24, 2018 · cfdf475 · cfdf475
1 parent 46dfa1d
commit cfdf475
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/prelude/Prelude.sawcore b/prelude/Prelude.sawcore
@@ -914,6 +914,11 @@ natCase :: (p :: Nat -> sort 0) -> p Zero -> ((n :: Nat) -> p (Succ n)) ->
            (n :: Nat) -> p n;
 natCase p z s = Nat__rec p z (\ (n::Nat) -> \ (r::p n) -> s n);
 
+-- An if-then-else for whether a Nat = 0
+if0Nat :: (a :: sort 0) -> Nat -> a -> a -> a;
+if0Nat a n x y = natCase (\ (_::Nat) -> a) x (\ (_::Nat) -> y) n;
+
+
 --------------------------------------------------------------------------------
 -- "Vec n a" is an array of n elements, each with type "a".
 primitive Vec :: Nat -> sort 0 -> sort 0;