Merge pull request #156 from GaloisInc/list-type

Add an inductive `List` datatype to the saw-core prelude.
GaloisInc · Feb 1, 2021 · 3927990 · 3927990
2 parents 06e6149 + 312907f
commit 3927990
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore
@@ -1409,6 +1409,22 @@ Sigma_proj2 (a : sort 0) (b : a -> sort 0)
       (\ (pa : a) (pb : b pa) -> pb);
 
 
+--------------------------------------------------------------------------------
+-- Lists
+
+data List (a : sort 0) : sort 0
+  where {
+    Nil : List a;
+    Cons : a -> List a -> List a;
+  }
+
+List__rec :
+  (a : sort 0) -> (P : List a -> sort 0) -> P (Nil a) ->
+  ((x : a) -> (l : List a) -> P l -> P (Cons a x l)) ->
+  (l : List a) -> P l;
+List__rec a P f1 f2 l = List#rec a P f1 f2 l;
+
+
 --------------------------------------------------------------------------------
 -- Computation monad