agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.41k stars 339 forks source link

`ModuleDoesntExport` has imprecise deadcode highlighting #7202

Closed andreasabel closed 3 months ago

andreasabel commented 3 months ago

With standard library v2.0:

open import Data.Bool.Properties  public using (∨-∧-isBooleanAlgebra)
open import Algebra.Lattice.Structures public using
  ( module IsBooleanAlgebra
  )
open IsBooleanAlgebra ∨-∧-isBooleanAlgebra public using
  ( ∧-cong; ∧-comm; ∧-assoc
  ; ∨-cong; ∨-comm; ∨-assoc
  ; ∨-∧-distribʳ
  ; isDistributiveLattice
  )
warning: -W[no]ModuleDoesntExport
The module _ doesn't export the following:
  ∨-∧-distribʳ 
...

The highlighting is imprecise:

Screenshot 2024-03-24 at 20 16 22

Should only highlight the name that isn't exported.