]> matita.cs.unibo.it Git - fireball-separation.git/blob - ocaml/pure.mli
Detection of divergents
[fireball-separation.git] / ocaml / pure.mli
1 module Pure :
2   sig
3     type t = V of int | A of t * t | L of t | B
4     val print : ?l:string list -> t -> string
5     val lift : int -> t -> t
6     val mwhd : (('a * t * ('b list as 'c) as 'b) list as 'a) * t * 'c -> t
7     val omega : bool -> t
8     val diverged : t -> bool
9   end
10
11 module Scott :
12   sig
13     val mk_n : int -> Pure.t
14     val dummy : Pure.t
15     val mk_match : Pure.t -> (int * Pure.t) list -> Pure.t
16   end