Module Exp.E

module E: sig .. end

val zero : Exp.exp
val one : Exp.exp
val tid : Exp.exp
val empty_list : Exp.exp
val empty_set : Exp.exp
val undef : Exp.exp
val num : int -> Exp.exp
val id : Exp.Id.t -> Exp.exp
val band : Exp.exp list -> Exp.exp
val bnot : Exp.exp -> Exp.exp
val fun1 : Exp.sfn1 -> Exp.exp -> Exp.exp
val fun2 : Exp.sfn2 -> Exp.exp -> Exp.exp -> Exp.exp
val funn : Exp.sfn -> Exp.exp list -> Exp.exp
val xor : Exp.exp list -> Exp.exp
val add : Exp.exp -> Exp.exp -> Exp.exp
val sub : Exp.exp -> Exp.exp -> Exp.exp
val list : Exp.exp list -> Exp.exp
val set : Exp.exp list -> Exp.exp
val item : Exp.exp -> Exp.exp
val items : Exp.exp -> Exp.exp -> Exp.exp
val eq : Exp.exp -> Exp.exp -> Exp.exp
val neq : Exp.exp -> Exp.exp -> Exp.exp
val ltn : Exp.exp -> Exp.exp -> Exp.exp
val leq : Exp.exp -> Exp.exp -> Exp.exp
val not_in_list : Exp.exp -> Exp.exp -> Exp.exp
val once_in_list : Exp.exp -> Exp.exp -> Exp.exp
val fv : Exp.exp -> Exp.IdSet.t -> Exp.IdSet.t
fv e s = fv(e) ++ s
val fhd : Exp.exp -> Exp.IdSet.t -> Exp.IdSet.t
val exfv : Exp.exp -> Exp.IdSet.t -> Exp.IdSet.t
fv e s = IdSet.filter is_existential (fv(e)) ++ s
val gensym_str : string -> Exp.exp
val gensym_str_ex : string -> Exp.exp
val forall_fv : (Exp.Id.t -> bool) -> Exp.exp -> bool
Imprint | Data protection