equal
deleted
inserted
replaced
278 | thf_sequent (( thf_sequent )) |
278 | thf_sequent (( thf_sequent )) |
279 |
279 |
280 thf_logic_formula : thf_binary_formula (( thf_binary_formula )) |
280 thf_logic_formula : thf_binary_formula (( thf_binary_formula )) |
281 | thf_unitary_formula (( thf_unitary_formula )) |
281 | thf_unitary_formula (( thf_unitary_formula )) |
282 | thf_type_formula (( THF_typing thf_type_formula )) |
282 | thf_type_formula (( THF_typing thf_type_formula )) |
283 | thf_subtype (( THF_type thf_subtype )) |
283 | thf_subtype (( Type_fmla thf_subtype )) |
284 |
284 |
285 thf_binary_formula : thf_binary_pair (( thf_binary_pair )) |
285 thf_binary_formula : thf_binary_pair (( thf_binary_pair )) |
286 | thf_binary_tuple (( thf_binary_tuple )) |
286 | thf_binary_tuple (( thf_binary_tuple )) |
287 | thf_binary_type (( THF_type thf_binary_type )) |
287 | thf_binary_type (( Type_fmla thf_binary_type )) |
288 |
288 |
289 thf_binary_pair : thf_unitary_formula thf_pair_connective thf_unitary_formula (( |
289 thf_binary_pair : thf_unitary_formula thf_pair_connective thf_unitary_formula (( |
290 Fmla (thf_pair_connective, [thf_unitary_formula1, thf_unitary_formula2]) |
290 Fmla (thf_pair_connective, [thf_unitary_formula1, thf_unitary_formula2]) |
291 )) |
291 )) |
292 |
292 |
466 tff_top_level_type : tff_atomic_type (( tff_atomic_type )) |
466 tff_top_level_type : tff_atomic_type (( tff_atomic_type )) |
467 | tff_mapping_type (( tff_mapping_type )) |
467 | tff_mapping_type (( tff_mapping_type )) |
468 | tff_quantified_type (( tff_quantified_type )) |
468 | tff_quantified_type (( tff_quantified_type )) |
469 |
469 |
470 tff_quantified_type : DEP_PROD LBRKT tff_variable_list RBRKT COLON tff_monotype (( |
470 tff_quantified_type : DEP_PROD LBRKT tff_variable_list RBRKT COLON tff_monotype (( |
471 Fmla_type (Quant (Dep_Prod, tff_variable_list, THF_type tff_monotype)) |
471 Fmla_type (Quant (Dep_Prod, tff_variable_list, Type_fmla tff_monotype)) |
472 )) |
472 )) |
473 | LPAREN tff_quantified_type RPAREN (( tff_quantified_type )) |
473 | LPAREN tff_quantified_type RPAREN (( tff_quantified_type )) |
474 |
474 |
475 tff_monotype : tff_atomic_type (( tff_atomic_type )) |
475 tff_monotype : tff_atomic_type (( tff_atomic_type )) |
476 | LPAREN tff_mapping_type RPAREN (( tff_mapping_type )) |
476 | LPAREN tff_mapping_type RPAREN (( tff_mapping_type )) |
478 tff_unitary_type : tff_atomic_type (( tff_atomic_type )) |
478 tff_unitary_type : tff_atomic_type (( tff_atomic_type )) |
479 | LPAREN tff_xprod_type RPAREN (( tff_xprod_type )) |
479 | LPAREN tff_xprod_type RPAREN (( tff_xprod_type )) |
480 |
480 |
481 tff_atomic_type : atomic_word (( Atom_type atomic_word )) |
481 tff_atomic_type : atomic_word (( Atom_type atomic_word )) |
482 | defined_type (( Defined_type defined_type )) |
482 | defined_type (( Defined_type defined_type )) |
483 | atomic_word LPAREN tff_type_arguments RPAREN (( Fmla_type (Fmla (Uninterpreted atomic_word, (map THF_type tff_type_arguments))) )) |
483 | atomic_word LPAREN tff_type_arguments RPAREN (( Fmla_type (Fmla (Uninterpreted atomic_word, (map Type_fmla tff_type_arguments))) )) |
484 | variable_ (( Fmla_type (Pred (Interpreted_ExtraLogic Apply, [Term_Var variable_])) )) |
484 | variable_ (( Fmla_type (Pred (Interpreted_ExtraLogic Apply, [Term_Var variable_])) )) |
485 |
485 |
486 tff_type_arguments : tff_atomic_type (( [tff_atomic_type] )) |
486 tff_type_arguments : tff_atomic_type (( [tff_atomic_type] )) |
487 | tff_atomic_type COMMA tff_type_arguments (( tff_atomic_type :: tff_type_arguments )) |
487 | tff_atomic_type COMMA tff_type_arguments (( tff_atomic_type :: tff_type_arguments )) |
488 |
488 |