aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4582.v
blob: 0842fb8fa7c985b50c9b4bf316afd98ae2f9306a (plain)
1
2
3
4
5
6
7
8
9
10
Require List.
Import List.ListNotations.

Variable Foo : nat -> nat.

Delimit Scope Foo_scope with F.

Notation " [ x ] " := (Foo x) : Foo_scope.

Check ([1] : nat)%F.