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     val env_of_sigma : int -> (int * t) list -> (('a * t * ('b list as 'c) as 'b) list as 'a)
  10   end
  11
  12 module Scott :
  13   sig
  14     val mk_n : int -> Pure.t
  15     val dummy : Pure.t
  16     val mk_match : Pure.t -> (int * Pure.t) list -> Pure.t
  17   end