aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/locate.out
blob: 1ceec7c9f82b2493d6fa321dd145cb53b7d211ba (plain)
1
2
3
4
5
6
7
8
9
10
11
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)