aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/locate.out
blob: 143eb1a1ae5411a971272bf66f67996b02405699 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
Notation
"b1 && b2" := if b1 then b2 else false (default interpretation)
"x && y" := andb x y : bool_scope
Notation
"'U' t" := S t (default interpretation)
Notation
"'_' t" := S t (default interpretation)
Notation
"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope (default interpretation)
Notation
"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope (default interpretation)
Notation
"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope (default interpretation)
Notation
"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope (default interpretation)