diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-17 15:55:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-17 16:03:06 +0200 |
| commit | 502d901fee12f07c31c2ea8b8c1455f74876d986 (patch) | |
| tree | 7e1370e89bf72bdc9d0b5762bcddc45ffb93ad20 /test-suite/success/CaseInClause.v | |
| parent | 8adcc8d26a200a5e52cf0413b6672aa63f9d6ea2 (diff) | |
Example illustrating non-local inference of the default type of impossible branches (see PR #323).
Diffstat (limited to 'test-suite/success/CaseInClause.v')
| -rw-r--r-- | test-suite/success/CaseInClause.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/success/CaseInClause.v b/test-suite/success/CaseInClause.v index 599b9566c..6424fe92d 100644 --- a/test-suite/success/CaseInClause.v +++ b/test-suite/success/CaseInClause.v @@ -24,3 +24,6 @@ Theorem foo : forall (n m : nat) (pf : n = m), (* 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. |