1074 | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args |
1074 | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args |
1075 | (false, s) => |
1075 | (false, s) => |
1076 if is_tptp_equal s andalso length args = 2 then |
1076 if is_tptp_equal s andalso length args = 2 then |
1077 IConst (`I tptp_equal, T, []) |
1077 IConst (`I tptp_equal, T, []) |
1078 else |
1078 else |
1079 (* Use a proxy even for partially applied THF0 equality, |
1079 (* Eta-expand partially applied THF equality, because the |
1080 because the LEO-II and Satallax parsers complain about not |
1080 LEO-II and Satallax parsers complain about not being able to |
1081 being able to infer the type of "=". *) |
1081 infer the type of "=". *) |
1082 IConst (proxy_base |>> prefix const_prefix, T, T_args) |
1082 let val i_T = domain_type T in |
|
1083 IAbs ((`I "X", i_T), |
|
1084 IAbs ((`I "Y", i_T), |
|
1085 IApp (IApp (IConst (`I tptp_equal, T, []), |
|
1086 IConst (`I "X", i_T, [])), |
|
1087 IConst (`I "Y", i_T, [])))) |
|
1088 end |
1083 | _ => IConst (name, T, []) |
1089 | _ => IConst (name, T, []) |
1084 else |
1090 else |
1085 IConst (proxy_base |>> prefix const_prefix, T, T_args) |
1091 IConst (proxy_base |>> prefix const_prefix, T, T_args) |
1086 | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args |
1092 | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args |
1087 else IConst (name, T, T_args)) |
1093 else IConst (name, T, T_args)) |