matita/contribs/LOGIC/datatypes_defs/Sequent.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 (* SEQUENTS
  18    - Naming policy:
  19      - left hand sides  (lhs): A C
  20      - right hand sides (rhs): B D
  21      - sequents              : R S
  22 *)
  23
  24 include "datatypes_defs/Formula.ma".
  25
  26 inductive LHS: Type \def
  27    | lleaf: LHS
  28    | labst: LHS \to Formula \to LHS
  29 .
  30
  31 inductive RHS: Type \def
  32    | rleaf: RHS
  33    | rabst: Formula \to RHS \to RHS
  34 .
  35
  36 inductive Sequent: Type \def
  37    | pair: LHS \to RHS \to Sequent
  38 .
  39
  40 definition linj: Formula \to LHS \def labst lleaf.
  41
  42 definition rinj: Formula \to RHS \def \lambda b. rabst b rleaf.
  43
  44 coercion cic:/matita/LOGIC/datatypes_defs/Sequent/linj.con.
  45
  46 coercion cic:/matita/LOGIC/datatypes_defs/Sequent/rinj.con.