Stdlib

.gitignore

@@ -3,3 +3,12 @@ _build/
 _opam/
 *.install
 *.merlin
+*.d
+.lia.cache
+*.conf
+*.vo
+*.vok
+*.vos
+*.aux
+*.glob
+*.gospel

CHANGES.md

@@ -9,6 +9,9 @@
 
 - Remove support for the record update syntax
   [\#428](https://github.com/ocaml-gospel/gospel/pull/428)
+- Rewrote the Gospel standard library to focus on the definition of
+  mathematical objects.
+  [\#423] (https://github.com/ocaml-gospel/gospel/pull/423)
 - Fix typing of expression with inlined record
   [\#420](https://github.com/ocaml-gospel/gospel/pull/420)
 - Improve error message for unbound record fields

README.md

@@ -116,9 +116,9 @@ starting with the `@` symbol:
 ```ocaml
 val max_array: int array -> int
 (*@ m = max_array a
-    requires Array.length a > 0
-    ensures forall i. 0 <= i < Array.length a -> a.(i) <= m
-    ensures exists i. 0 <= i < Array.length a /\ a.(i) = m *)
+    requires Sequence.length a > 0
+    ensures forall i. 0 <= i < Sequence.length a -> a[i] <= m
+    ensures exists i. 0 <= i < Sequence.length a /\ a[i] = m *)
 ```
 
 Gospel provides a type-checker that ensures that your specifications are

docs/docs/faq.md

@@ -37,7 +37,7 @@ every possible array:
 val total_weight : weight:('a array -> int) -> ('a array) list -> int
 (*@ y = total_weight ~weight l
     requires forall a. weight a >= 0
-    ensures y = List.fold_left (fun acc a -> acc + weight a) 0 l *)
+    ensures y = Sequence.fold_left (fun acc a -> acc + weight a) 0 l *)
 ```
 
 <hr />

docs/docs/language/constant-specifications.md

@@ -15,7 +15,7 @@ Here is an example:
 
 ```ocaml
 val argv : string array
-(*@ ensures Array.length argv >= 1 *)
+(*@ ensures Sequence.length argv >= 1 *)
 ```
 
 These clauses hold at the end of the surrounding module evaluation.

docs/docs/language/logical.md

@@ -12,8 +12,8 @@ comments. Here is a typical example:
 
 ```ocaml
 (*@ predicate is_sorted (a: int array) =
-      forall i j. 0 <= i <= j < Array.length a
-                  -> a.(i) <= a.(j) *)
+      forall i j. 0 <= i <= j < Sequence.length a
+                  -> a[i] <= a[j] *)
 ```
 
 We can then reuse the predicate `is_sorted` inside any Gospel annotations such