exception Choice_not_found of string Lazy.t
(** register a new number choice *)
-val add_num_choice: codomain_item -> unit
+val add_num_choice: Cic.term codomain_item -> unit
(** {2 Choices lookup}
* for user defined aliases *)
-val lookup_num_choices: unit -> codomain_item list
+val lookup_num_choices: unit -> Cic.term codomain_item list
(** @param dsc description (1st component of codomain_item) *)
-val lookup_num_by_dsc: string -> codomain_item
+val lookup_num_by_dsc: string -> Cic.term 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
+val lookup_symbol_by_dsc:
+ mk_appl: ('term list -> 'term) ->
+ mk_implicit: (bool -> 'term) ->
+ term_of_uri: (UriManager.uri -> 'term) ->
+ string -> string -> 'term codomain_item
+
+val cic_lookup_symbol_by_dsc:
+ string -> string -> Cic.term codomain_item
val mk_choice:
+ mk_appl: ('term list -> 'term) ->
+ mk_implicit: (bool -> 'term) ->
+ term_of_uri: (UriManager.uri -> 'term) ->
string * CicNotationPt.argument_pattern list *
CicNotationPt.cic_appl_pattern ->
- codomain_item
+ 'term codomain_item