diff options
Diffstat (limited to 'test-suite/output/Notations.out')
| -rw-r--r-- | test-suite/output/Notations.out | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index beba8df9..66307236 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -127,3 +127,12 @@ Identifier 'foo' now a keyword : nat fun _ : nat => 9 : nat -> nat +Identifier 'ONE' now a keyword +fun (x : nat) (p : x = x) => match p with + | ONE => ONE + end = p + : forall x : nat, x = x -> Prop +fun (x : nat) (p : x = x) => match p with + | 1 => 1 + end = p + : forall x : nat, x = x -> Prop |