✨ Add coq.univ.super

LPCIC · Nov 21, 2022 · 1eb52ba · 1eb52ba
1 parent aa3f4b4
commit 1eb52ba
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 0 deletions.
diff --git a/coq-builtin.elpi b/coq-builtin.elpi
@@ -950,6 +950,9 @@ external pred coq.univ.print .
 % [coq.univ.new U] A fresh universe.
 external pred coq.univ.new o:univ.
 
+% [coq.univ.super U U1] relates a univ U to its successor U1
+external pred coq.univ.super i:univ, o:univ.
+
 % [coq.univ Name U] Finds a named unvierse. Can fail.
 external pred coq.univ o:id, o:univ.
 

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
@@ -2236,6 +2236,14 @@ phase unnecessary.|};
      state, !: u, [])),
   DocAbove);
 
+  MLCode(Pred("coq.univ.super",
+    In(univ,"U",
+    Out(univ,"U1",
+    Full(unit_ctx,  "relates a univ U to its successor U1"))),
+  (fun u _ ~depth _ _ state ->
+    state, !: (Univ.Universe.super u), [])),
+  DocAbove);
+
   MLCode(Pred("coq.univ",
     InOut(B.ioarg id, "Name",
     InOut(B.ioarg univ, "U",