diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /test-suite/ideal-features/Case3.v |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'test-suite/ideal-features/Case3.v')
-rw-r--r-- | test-suite/ideal-features/Case3.v | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/test-suite/ideal-features/Case3.v b/test-suite/ideal-features/Case3.v new file mode 100644 index 00000000..e9dba1e3 --- /dev/null +++ b/test-suite/ideal-features/Case3.v @@ -0,0 +1,28 @@ +Inductive Le : nat->nat->Set := + LeO: (n:nat)(Le O n) +| LeS: (n,m:nat)(Le n m) -> (Le (S n) (S m)). + +Parameter iguales : (n,m:nat)(h:(Le n m))Prop . + +Type <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of + (LeO O) => True + | (LeS (S x) (S y) H) => (iguales (S x) (S y) H) + | _ => False end. + + +Type <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of + (LeO O) => True + | (LeS (S x) O H) => (iguales (S x) O H) + | _ => False end. + +Parameter discr_l : (n:nat) ~((S n)=O). + +Type +[n:nat] + <[n:nat]n=O\/~n=O>Cases n of + O => (or_introl ? ~O=O (refl_equal ? O)) + | (S O) => (or_intror (S O)=O ? (discr_l O)) + | (S (S x)) => (or_intror (S (S x))=O ? (discr_l (S x))) + + end. + |