+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 ]))
+