diff options
author | 2016-07-19 13:19:34 +0200 | |
---|---|---|
committer | 2016-07-19 13:45:23 +0200 | |
commit | f7ae4e6433e44a0b3a838847c58ab72ffffa3d48 (patch) | |
tree | f05d58a6f51c77ce890452ff00babd8cadf2e990 /test-suite/output/PatternsInBinders.v | |
parent | a67bd7f93224c61b6a59459ea1114a6670daa857 (diff) |
Some extra fixes in printing patterns in binders.
- typo in notation_ops.ml
- factorization of patterns in ppconstr.ml
- update of test-suite
- printing of cast of a binding pattern if in mode "printing all"
The question of whether or not to print the type of a binding pattern
by default seems open to me.
Diffstat (limited to 'test-suite/output/PatternsInBinders.v')
-rw-r--r-- | test-suite/output/PatternsInBinders.v | 32 |
1 files changed, 21 insertions, 11 deletions
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index 8911909ab..b5c91e347 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -21,7 +21,20 @@ Print foo. Definition baz '(Bar n1 b1 tt p1) '(Bar n2 b2 tt p2) := n1+p1. Print baz. -(** Some test involving unicode noations. *) +Module WithParameters. + +Definition swap {A B} '((x,y) : A*B) := (y,x). +Print swap. + +Check fun (A B:Type) '((x,y) : A*B) => swap (x,y) = (y,x). +Check forall (A B:Type) '((x,y) : A*B), swap (x,y) = (y,x). + +Check exists '((x,y):A*A), swap (x,y) = (y,x). +Check exists '((x,y):A*A) '(z,w), swap (x,y) = (z,w). + +End WithParameters. + +(** Some test involving unicode notations. *) Module WithUnicode. Require Import Coq.Unicode.Utf8. @@ -31,24 +44,21 @@ Module WithUnicode. End WithUnicode. - (** * Suboptimal printing *) -(** These tests show examples which expose the [let] introduced by - the pattern notation in binders. *) - Module Suboptimal. -Definition swap {A B} '((x,y) : A*B) := (y,x). -Print swap. - -Check forall (A B:Type) '((x,y) : A*B), swap (x,y) = (y,x). - -Check exists '((x,y):A*A), swap (x,y) = (y,x). +(** This test shows an example which exposes the [let] introduced by + the pattern notation in binders. *) Inductive Fin (n:nat) := Z : Fin n. Definition F '(n,p) : Type := (Fin n * Fin p)%type. Definition both_z '(n,p) : F (n,p) := (Z _,Z _). Print both_z. +(** These tests show examples which do not factorize binders *) + +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. |