open DisambiguateTypes
-(** {2 Choice registration interface} *)
-
- (** to be raised when a choice is invalid due to some given parameter (e.g.
- * wrong number of Cic.term arguments received) *)
-exception Invalid_choice
+(** {2 Choice registration low-level interface} *)
(** raised by lookup_XXXX below *)
-exception Choice_not_found of string
-
- (** register a new symbol choice *)
-val add_symbol_choice: string -> codomain_item -> unit
+exception Choice_not_found of string Lazy.t
(** register a new number choice *)
val add_num_choice: codomain_item -> unit
(** {2 Choices lookup}
* for user defined aliases *)
- (** @param symbol symbol as per AST *)
-val lookup_symbol_choices: string -> codomain_item list
-
val lookup_num_choices: unit -> codomain_item list
+ (** @param dsc description (1st component of codomain_item) *)
+val lookup_num_by_dsc: string -> codomain_item
+
(** @param symbol symbol as per AST
* @param dsc description (1st component of codomain_item)
*)
val lookup_symbol_by_dsc: string -> string -> codomain_item
- (** @param dsc description (1st component of codomain_item) *)
-val lookup_num_by_dsc: string -> codomain_item
+val mk_choice:
+ string * CicNotationPt.argument_pattern list *
+ CicNotationPt.cic_appl_pattern ->
+ codomain_item