-let add_symbol_choice symbol codomain_item =
- let current_choices =
- try
- Hashtbl.find symbol_choices symbol
- with Not_found -> []
- 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 ]))
-