Previous  Up  Next

Module Apply


module Apply: sig  end
evaluation, not affecting function bodies
val abs : Sym.t
val apply : Dom.t option -> Sym.t
Parameters:
r : Dom.t option
 
val mk_abs : Term.t -> Term.t
Parameters:
a : Term.t
 
val mk_apply : (Sym.t -> Term.t list -> Term.t) ->
       Dom.t option -> Term.t -> Term.t list -> Term.t
Parameters:
sigma : Sym.t -> Term.t list -> Term.t
r : Dom.t option
a : Term.t
al : Term.t list

evaluation, not affecting function bodies

val eval : (Sym.t -> Term.t list -> Term.t) -> Term.t -> Term.t
Parameters:
sigma : Sym.t -> Term.t list -> Term.t
 
val byValue : (Sym.t -> Term.t list -> Term.t) -> Term.t -> Term.t
Parameters:
sigma : Sym.t -> Term.t list -> Term.t
a : Term.t
 
val hnf : (Sym.t -> Term.t list -> Term.t) -> Term.t -> Term.t
Parameters:
sigma : Sym.t -> Term.t list -> Term.t
a : Term.t
 
val byName : (Sym.t -> Term.t list -> Term.t) -> Term.t -> Term.t
Parameters:
sigma : Sym.t -> Term.t list -> Term.t
a : Term.t
 
val subst : (Sym.t -> Term.t list -> Term.t) -> Term.t -> Term.t -> int -> Term.t
Parameters:
sigma : Sym.t -> Term.t list -> Term.t
a : Term.t
s : Term.t
k : int
 
val substl : (Sym.t -> Term.t list -> Term.t) ->
       Term.t list -> Term.t -> int -> Term.t list
Parameters:
sigma : Sym.t -> Term.t list -> Term.t
al : Term.t list
s : Term.t
k : int
 
val lift : Term.t -> int -> Term.t
Parameters:
a : Term.t
k : int
 
val liftl : Term.t list -> int -> Term.t list
Parameters:
al : Term.t list
k : int
 
val sigma : Sym.apply -> Term.t list -> Term.t
Parameters:
op : Sym.apply
al : Term.t list
 
val map : (Term.t -> Term.t) -> Term.t -> Term.t
Parameters:
f : Term.t -> Term.t
a : Term.t