]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/pure.mli
New interesting example
[fireball-separation.git] / ocaml / pure.mli
index f36007498ca1556eeb20708641560cef3b725cc3..9b683b33530ccadf28c87ad43dcb7af137e85541 100644 (file)
@@ -1,10 +1,12 @@
 module Pure :
   sig
-    type t = V of int | A of t * t | L of t
+    type t = V of int | A of t * t | L of t | B
     val print : ?l:string list -> t -> string
     val lift : int -> t -> t
-    val unwind : ?tbl:('a list * t * 'a list as 'a, t) Hashtbl.t -> 'a -> t
     val mwhd : (('a * t * ('b list as 'c) as 'b) list as 'a) * t * 'c -> t
+    val omega : bool -> t
+    val diverged : t -> bool
+    val env_of_sigma : int -> (int * t) list -> (('a * t * ('b list as 'c) as 'b) list as 'a)
   end
 
 module Scott :