aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/ideal-features/Case3.v
blob: de7784aec5863dc543ff505116d30931c3f17ecd (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
Inductive Le : nat -> nat -> Set :=
  | LeO : forall n : nat, Le 0 n
  | LeS : forall n m : nat, Le n m -> Le (S n) (S m).

Parameter discr_l : forall n : nat, S n <> 0.

Type
  (fun n : nat =>
   match n return (n = 0 \/ n <> 0) with
   | O => or_introl (0 <> 0) (refl_equal 0)
   | S O => or_intror (1 = 0) (discr_l 0)
   | S (S x) => or_intror (S (S x) = 0) (discr_l (S x))
   end).

Parameter iguales : forall (n m : nat) (h : Le n m), Prop.

Type
  match LeO 0 as h in (Le n m) return Prop with
  | LeO O => True
  | LeS (S x) (S y) H => iguales (S x) (S y) H
  | _ => False
  end.

Type
  match LeO 0 as h in (Le n m) return Prop with
  | LeO O => True
  | LeS (S x) O H => iguales (S x) 0 H
  | _ => False
  end.