File: boundvars.v

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (14 lines) | stat: -rw-r--r-- 621 bytes parent folder | download | duplicates (6)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
(* An example showing a bug in the detection of free variables *)
(* "x" is not free in the common type of "x" and "y" *)

Check forall (x z:unit) (x y : match z as x return x=x with tt => eq_refl end = eq_refl), x=x.

(* An example showing a bug in the detection of bound variables *)

Goal forall x, match x return x = x with 0 => eq_refl | _ => eq_refl end = eq_refl.
intro.
match goal with
|- (match x as y in nat return y = y with O => _ | S n => _ end) = _ => assert (forall y, y = 0) end.
intro.
Check x0. (* Check that "y" has been bound to "x0" while matching "match x as x0 return x0=x0 with ... end" *)
Abort.