Module Theory.Sigma

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)