-
Notifications
You must be signed in to change notification settings - Fork 251
Closed
Labels
breakingbuglibrary-designstatus: duplicateThe main contents of the issue or PR already exists in another issue or PR.The main contents of the issue or PR already exists in another issue or PR.
Milestone
Description
The module parameter setup just doesn't work. When you write
open import Function.Definitions
you still get e.g. Surjective
in scope with two equality parameters instead of one.
I think the best plan is to ditch the module parameters in Function.Definitions
entirely, and fold Core1
and Core2
into it.
Metadata
Metadata
Assignees
Labels
breakingbuglibrary-designstatus: duplicateThe main contents of the issue or PR already exists in another issue or PR.The main contents of the issue or PR already exists in another issue or PR.