diff options
| author | Hugo Herbelin | 2017-11-25 20:50:03 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:07 +0100 |
| commit | dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 (patch) | |
| tree | 48bc1c2a7aef0498290e55917323dcc484e2e878 /test-suite/output/Notations3.out | |
| parent | 8f93f9a2df6e17386f46f79b2a7eda4104d0a94e (diff) | |
Notations: Adding modifiers to tell which kind of binder a constr can parse.
Concretely, we provide "constr as ident", "constr as strict pattern"
and "constr as pattern".
This tells to parse a binder as a constr, restricting to only ident or
to only a strict pattern, or to a pattern which can also be an ident.
The "strict pattern" modifier allows to restrict the use of patterns
in printing rules. This allows e.g. to select the appropriate rule for
printing between {x|P} and {'pat|P}.
Diffstat (limited to 'test-suite/output/Notations3.out')
| -rw-r--r-- | test-suite/output/Notations3.out | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 6d195b5122..3fd4c1c311 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -194,8 +194,6 @@ pair (prod nat (prod nat nat))) (prod (prod nat nat) nat) fun x : nat => if x is n .+ 1 then n else 1 : nat -> nat -{{{x, y}} : nat * nat | x + y = 0} - : Set exists2' {{x, y}}, x = 0 & y = 0 : Prop exists2 x : nat * nat, |