Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal-General/nominal_library.ML
changeset 2407 49ab06c0ca64
parent 2399 107c06267f33
child 2408 f1980f89c405 
--- a/Nominal-General/nominal_library.ML	Tue Aug 17 07:11:45 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Tue Aug 17 17:52:25 2010 +0800
@@ -41,12 +41,12 @@
   val fold_conj: term list -> term
 
   (* datatype operations *)
+  type cns_info = (term * typ * typ list * bool list) list
+
   val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list
   val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ
-  val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> 
-    (term * typ * typ list * bool list) list list
-  val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> 
-    (term * typ * typ list * bool list) list
+  val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list
+  val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> cns_info
   val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list
 
   (* tactics for function package *)
@@ -130,6 +130,8 @@
 
 (** datatypes **)
 
+(* constructor infos *)
+type cns_info = (term * typ * typ list * bool list) list
 
 (* returns the type of the nth datatype *)
 fun all_dtyps descr sorts =
nominal2