Skip to content

Conversation

@MatthewDaggitt
Copy link
Collaborator

Deprecates and cleans up the imports

Relation.Nullary.Product
Relation.Nullary.Sum
Relation.Nullary.Implication

@MatthewDaggitt MatthewDaggitt added this to the v2.0 milestone Oct 26, 2022
@MatthewDaggitt MatthewDaggitt changed the title State 2 of refactoring of Relation.Nullary Stage 2 of refactoring of Relation.Nullary Oct 26, 2022
@MatthewDaggitt MatthewDaggitt merged commit 7602ca3 into master Oct 30, 2022
@MatthewDaggitt MatthewDaggitt deleted the nullary-deprecation branch October 30, 2022 13:10
@jamesmckinna
Copy link
Collaborator

jamesmckinna commented Oct 30, 2022

Asleep at the wheel, so I missed these:

  • Relation.Nullary.Negation.Core has two redundant imports
  • open import Data.Bool.Base using (not)
  • open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)

Suggest a second round of import-bashing through this PR and its predecessor #1855?
UPDATED Additionally, can tighten those for

  • Relation/Nullary/Decidable.agda
  • Relation/Nullary/Negation.agda
  • Relation/Nullary/Reflects.agda

@MatthewDaggitt
Copy link
Collaborator Author

Sorry, only just seen this. Yes, would welcome these import changes 👍

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants