helm/matita/tests/match_inference.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 set "baseuri" "cic:/matita/tests/match_inference/".
  16
  17 inductive pos: Set \def
  18 | one : pos
  19 | next : pos \to pos.
  20
  21 inductive nat:Set \def
  22 | O : nat
  23 | S : nat \to nat.
  24
  25 definition pos2nat : pos \to nat  \def
  26      \lambda x:pos . match x with
  27       [ one \Rightarrow O
  28       | (next z) \Rightarrow O].
  29
  30 inductive empty (x:nat) : nat \to Set \def .
  31
  32 definition empty2nat : (empty O O) \to nat  \def
  33   \lambda x : (empty O O). S (match x in empty with []).
  34
  35 inductive le (n:nat) : nat \to Prop \def
  36   | le_n : le n n
  37   | le_S : \forall m:nat. le n m \to le n (S m).
  38
  39 inductive True : Prop \def
  40  I : True.
  41
  42 definition r : True \def
  43  match (le_n O) with
  44   [ le_n \Rightarrow I
  45   | (le_S y p') \Rightarrow I ].
  46
  47 inductive Prod (A,B:Set): Set \def
  48 pair : A \to B \to Prod A B.
  49
  50 definition fst : \forall A,B:Set. (Prod A B) \to A \def
  51 \lambda A,B:Set. \lambda p:(Prod A B). match p with
  52 [(pair a b) \Rightarrow a].