module Sigma: sig
.. end
Environments
val add : Term.constr -> Term.constr -> Term.constr -> Term.constr -> Term.constr
add ty n x map
adds the value x
of type ty
with key n
in map
val empty : Term.constr -> Term.constr
empty ty
create an empty map of type ty
val of_list : Term.constr -> Term.constr -> (int * Term.constr) list -> Term.constr
of_list ty null l
translates an OCaml association list into a Coq one
val to_fun : Term.constr -> Term.constr -> Term.constr -> Term.constr
to_fun ty null map
converts a Coq association list into a Coq function (with default value null
)