From 80d36bc6538b7feaab3dfa43f6e234ae85b55692 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 5 Dec 2016 07:27:06 +0100 Subject: A test checking for non-collision of name in irrefutable patterns. --- test-suite/output/PatternsInBinders.out | 2 ++ test-suite/output/PatternsInBinders.v | 3 +++ 2 files changed, 5 insertions(+) (limited to 'test-suite') diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index c012a86b01..95be04c32c 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -37,3 +37,5 @@ fun '(x, y) '(z, t) => swap (x, y) = (z, t) : A * B -> B * A -> Prop forall '(x, y) '(z, t), swap (x, y) = (z, t) : Prop +fun (pat : nat) '(x, y) => x + y = pat + : nat -> nat * nat -> Prop diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index 6fa357a90c..0bad472f41 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -64,3 +64,6 @@ Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t). Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t). End Suboptimal. + +(** Test risk of collision for internal name *) +Check fun pat => fun '(x,y) => x+y = pat. -- cgit v1.2.3 From d2830ca4adf062df96d5e8978d4254cf5ece30c4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 5 Dec 2016 12:12:39 +0100 Subject: Supporting arbitrary binders in record fields, including e.g. patterns. --- test-suite/success/record_syntax.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'test-suite') diff --git a/test-suite/success/record_syntax.v b/test-suite/success/record_syntax.v index db2bbb0dc7..07a5bc0606 100644 --- a/test-suite/success/record_syntax.v +++ b/test-suite/success/record_syntax.v @@ -45,3 +45,11 @@ Record Foo := { foo : unit; }. Definition foo_ := {| foo := tt; |}. End E. + +Module F. + +Record Foo := { foo : nat * nat -> nat -> nat }. + +Definition foo_ := {| foo '(x,y) n := x+y+n |}. + +End F. -- cgit v1.2.3