[NSeq] Added the nseq_content builtin

colibri2/theories/nseq/nseq.ml

@@ -25,6 +25,7 @@ module Builtin = struct
     | NSeq
     | NSeq_first
     | NSeq_last
+    | NSeq_content
     | NSeq_length
     | NSeq_get
     | NSeq_set
@@ -56,6 +57,12 @@ module Builtin = struct
       (Dolmen_std.Path.global "nseq_last")
       (Expr.Ty.pi [ val_ty_var ] (Expr.Ty.arrow [ val_nseq_ty ] int_ty))
 
+  let nseq_content : Dolmen_std.Expr.term_cst =
+    Expr.Id.mk ~name:"nseq_content" ~builtin:NSeq_content
+      (Dolmen_std.Path.global "nseq_content")
+      (Expr.Ty.pi [ val_ty_var ]
+         (Expr.Ty.arrow [ val_nseq_ty ] (Expr.Ty.arrow [ int_ty ] val_ty)))
+
   let nseq_length : Dolmen_std.Expr.term_cst =
     Expr.Id.mk ~name:"nseq_length" ~builtin:NSeq_length
       (Dolmen_std.Path.global "nseq_length")
@@ -152,6 +159,8 @@ module Builtin = struct
             app1 env s nseq_first
         | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_last" } ->
             app1 env s nseq_last
+        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_content" } ->
+            app1 env s nseq_content
         | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_length" } ->
             app1 env s nseq_length
         | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_get" } ->