diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations4.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 3 |
2 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 807914a671..1c8f237bb8 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -14,6 +14,8 @@ Entry constr:myconstr is : nat [<< # 0 >>] : option nat +[2 + 3] + : nat [1 {f 1}] : Expr fun (x : nat) (y z : Expr) => [1 + y z + {f x}] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 2906698386..4ab800c9ba 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -22,6 +22,9 @@ Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr a Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9). Check [ << # 0 >> ]. +Notation "n" := n%nat (in custom myconstr at level 0, n bigint). +Check [ 2 + 3 ]. + End A. Module B. |