[Agda] missing import overlap

Sergei Meshveliani mechvel at botik.ru
Mon Jul 10 21:30:21 CEST 2017

Previous message (by thread): [Agda] how do I handle absurd with patterns?
Next message (by thread): [Agda] missing import overlap
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

People,
I wonder: given

  open import Relation.Nullary  
  open import Relation.Nullary using (yes; no)

Agda does not report an overlap. Needs it?

------
Sergei

Previous message (by thread): [Agda] how do I handle absurd with patterns?
Next message (by thread): [Agda] missing import overlap
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

More information about the Agda mailing list