CI #200
sanjit-bhatAnnotations
2 warnings
|
build-vos (dev):
external/iris/iris/bi/notation.v#L36
Closed notations (i.e. starting and ending with a terminal symbol) should usually be at level 0 (default).
|
|
build (dev):
external/iris/iris/bi/notation.v#L36
Closed notations (i.e. starting and ending with a terminal symbol) should usually be at level 0 (default).
|