equal
deleted
inserted
replaced
67 fun fn_isa_to_met "equal" = "=" |
67 fun fn_isa_to_met "equal" = "=" |
68 | fn_isa_to_met x = x; |
68 | fn_isa_to_met x = x; |
69 |
69 |
70 fun metis_lit b c args = (b, (c, args)); |
70 fun metis_lit b c args = (b, (c, args)); |
71 |
71 |
72 fun hol_type_to_fol (AtomV x) = Metis.Term.Var x |
72 fun hol_type_to_fol (TyVar x) = Metis.Term.Var x |
73 | hol_type_to_fol (AtomF x) = Metis.Term.Fn (x, []) |
73 | hol_type_to_fol (TyFree x) = Metis.Term.Fn (x, []) |
74 | hol_type_to_fol (Comp (tc, tps)) = |
74 | hol_type_to_fol (TyConstr (tc, tps)) = |
75 Metis.Term.Fn (tc, map hol_type_to_fol tps); |
75 Metis.Term.Fn (tc, map hol_type_to_fol tps); |
76 |
76 |
77 (*These two functions insert type literals before the real literals. That is the |
77 (*These two functions insert type literals before the real literals. That is the |
78 opposite order from TPTP linkup, but maybe OK.*) |
78 opposite order from TPTP linkup, but maybe OK.*) |
79 |
79 |