equal
deleted
inserted
replaced
368 fun is_format_typed (TFF _) = true |
368 fun is_format_typed (TFF _) = true |
369 | is_format_typed (THF _) = true |
369 | is_format_typed (THF _) = true |
370 | is_format_typed (DFG _) = true |
370 | is_format_typed (DFG _) = true |
371 | is_format_typed _ = false |
371 | is_format_typed _ = false |
372 |
372 |
|
373 fun is_format_with_fool (THF (With_FOOL, _, _)) = true |
|
374 | is_format_with_fool (TFF (With_FOOL, _)) = true |
|
375 | is_format_with_fool _ = false |
|
376 |
373 fun tptp_string_of_role Axiom = "axiom" |
377 fun tptp_string_of_role Axiom = "axiom" |
374 | tptp_string_of_role Definition = "definition" |
378 | tptp_string_of_role Definition = "definition" |
375 | tptp_string_of_role Lemma = "lemma" |
379 | tptp_string_of_role Lemma = "lemma" |
376 | tptp_string_of_role Hypothesis = "hypothesis" |
380 | tptp_string_of_role Hypothesis = "hypothesis" |
377 | tptp_string_of_role Conjecture = "conjecture" |
381 | tptp_string_of_role Conjecture = "conjecture" |
463 if s = tptp_empty_list then |
467 if s = tptp_empty_list then |
464 (* used for lists in the optional "source" field of a derivation *) |
468 (* used for lists in the optional "source" field of a derivation *) |
465 "[" ^ commas (map of_term ts) ^ "]" |
469 "[" ^ commas (map of_term ts) ^ "]" |
466 else if is_tptp_equal s then |
470 else if is_tptp_equal s then |
467 space_implode (" " ^ tptp_equal ^ " ") (map of_term ts) |
471 space_implode (" " ^ tptp_equal ^ " ") (map of_term ts) |
468 |> is_format_higher_order format ? parens |
472 |> (is_format_higher_order format orelse is_format_with_fool format) ? parens |
469 else if s = tptp_ho_forall orelse s = tptp_ho_exists then |
473 else if s = tptp_ho_forall orelse s = tptp_ho_exists then |
470 (case ts of |
474 (case ts of |
471 [AAbs (((s', ty), tm), [])] => |
475 [AAbs (((s', ty), tm), [])] => |
472 (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever |
476 (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever |
473 possible, to work around LEO-II 1.2.8 parser limitation. *) |
477 possible, to work around LEO-II 1.2.8 parser limitation. *) |