diff options
Diffstat (limited to 'test-suite/success/CaseInClause.v')
-rw-r--r-- | test-suite/success/CaseInClause.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/CaseInClause.v b/test-suite/success/CaseInClause.v index 3679eead..6424fe92 100644 --- a/test-suite/success/CaseInClause.v +++ b/test-suite/success/CaseInClause.v @@ -20,3 +20,10 @@ Theorem foo : forall (n m : nat) (pf : n = m), match pf in _ = N with | eq_refl => unit end. + +(* Check redundant clause is removed *) +Inductive I : nat * nat -> Type := C : I (0,0). +Check fun x : I (1,1) => match x in I (y,z) return y = z with C => eq_refl end. + +(* An example of non-local inference of the type of an impossible case *) +Check (fun y n (x:Vector.t nat (S n)) => match x with a::_ => a | _ => y end) 2. |