]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/registry/helm_registry.mli
- matex: minor corrections to handle applications with many arguments
[helm.git] / matita / components / registry / helm_registry.mli
index 68434603dbe4e08243203304f2aeb0ffb794af0d..29dd335faab474926b877f38d7d53864fda31f97 100644 (file)
@@ -134,6 +134,7 @@ val float:        string -> float
 val bool:         string -> bool
 val pair:         (string -> 'a) -> (string -> 'b) -> string -> 'a * 'b
 val triple:       (string -> 'a) -> (string -> 'b) -> (string -> 'c) -> string -> 'a * 'b * 'c
+val quad:         (string -> 'a) -> (string -> 'b) -> (string -> 'c) -> (string -> 'd) -> string -> 'a * 'b * 'c * 'd
 
 (** {3 Typed getters} *)
 
@@ -154,6 +155,9 @@ val get_pair: (string -> 'a) -> (string -> 'b) -> string -> 'a * 'b
   (** decode values which are blank separated list of values, of length 3 *)
 val get_triple: (string -> 'a) -> (string -> 'b) -> (string -> 'c) -> string -> 'a * 'b * 'c
 
+  (** decode values which are blank separated list of values, of length 4 *)
+val get_quad: (string -> 'a) -> (string -> 'b) -> (string -> 'c) -> (string -> 'd) -> string -> 'a * 'b * 'c * 'd
+
 (** {4 Shorthands} *)
 
 val get_string: string -> string