Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/agda/agda/issues/7202 below:

`ModuleDoesntExport` has imprecise deadcode highlighting · Issue #7202 · agda/agda · GitHub

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:

Should only highlight the name that isn't exported.

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