in
Hashtbl.replace symbol_choices symbol (codomain_item :: current_choices)
+let add_binary_op symbol dsc appl_head =
+ add_symbol_choice symbol
+ (dsc,
+ (fun env _ args ->
+ let t1, t2 =
+ match args with
+ | [t1; t2] -> t1, t2
+ | _ -> raise Invalid_choice
+ in
+ Cic.Appl [ appl_head; t1; t2 ]))
+
+let add_unary_op symbol dsc appl_head =
+ add_symbol_choice symbol
+ (dsc,
+ (fun env _ args ->
+ let t = match args with [t] -> t | _ -> raise Invalid_choice in
+ Cic.Appl [ appl_head; t ]))
+
let add_num_choice choice = num_choices := choice :: !num_choices
let lookup_symbol_choices symbol =
List.find (has_description dsc) !num_choices
with Not_found -> raise (Choice_not_found ("Num with dsc " ^ dsc))
+ (** initial table contents *)
+
+let _ =
+ add_binary_op "exists" "exists"
+ (Cic.MutInd (HelmLibraryObjects.Logic.ex_URI, 0, []))