let _ =
add_binary_op "exists" "exists"
- (Cic.MutInd (HelmLibraryObjects.Logic.ex_URI, 0, []))
+ (Cic.MutInd (HelmLibraryObjects.Logic.ex_URI, 0, []));
+ add_symbol_choice "cast"
+ ("type cast",
+ (fun env _ args ->
+ let t1, t2 =
+ match args with
+ | [t1; t2] -> t1, t2
+ | _ -> raise Invalid_choice
+ in
+ Cic.Cast (t1, t2)));
+