Agda raises a warning on an empty private block but not on a private block that contains a syntax declaration, even though the private does not seem to have any effect in this case.
module Test where
open import Agda.Builtin.Nat
module M
where
f : Nat → Nat
f x = x
private -- No warning is raised here.
syntax f x = [ x ]
h : Nat → Nat
h x = M.[ x ] -- This is accepted, showing that the [ ] syntax is not private.
The same is true for a fixity declaration in a private block.
_#_ : Nat → Nat → Nat x # y = x private -- No warning is raised here either. infixl 5 _#_
It would seem much more consistent and useful to me to warn about effectless private blocks and not just empty ones.
(Tested with Agda version 2.6.4.)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4