Closed
Description
First issue with RC 1. Changelog doesn't mention that the name of the operation in Semilattice changed from _∧_ to _∙_.
More problematically the names in IsSemilattice have not been changed 😢
Metadata
Metadata
Assignees
Type
Projects
Relationships
Development
Participants
Activity
[-]Missing CHANGELOG entry for change of `Semilattice` operation name[/-][+]Problems with change of `Semilattice` operation name[/+]Taneb commentedon Oct 26, 2023
I'd like to address this more aggressively, by tying it with #2138 and removing the undirected
IsLatticeetc structures entirely.•: in•-cong : Congruent₂ _•_inAlgebra.Consequences.Setoid#2178jamesmckinna commentedon Oct 26, 2023
Don't remove: deprecate!
jamesmckinna commentedon Nov 11, 2023
@Taneb Any progress on this issue/PR?
jamesmckinna commentedon Nov 20, 2023
Cf. #2178 what is the operator symbol supposed to be in
Semilattice?I'm starting to wonder/panic whether that PR actually did the right thing?
MatthewDaggitt commentedon Nov 24, 2023
Should be the dot symbol. In the interests of getting the next RC out the door I'm taking this one over.
Taneb commentedon Nov 24, 2023
Sorry, I've been sick lately. I'm only just getting enough brainpower back to write Agda now
IsSemilattice#2211MatthewDaggitt commentedon Nov 25, 2023
No worries, I hope you have a swift recovery!
jamesmckinna commentedon Nov 25, 2023
Get well soon! I've approved Matthew's PR in the interim.
Fixes #2166 by fixing names in `IsSemilattice` (#2211)
README.Data.Fin.Substitution.UntypedLambda#2279Fixes #2166 by fixing names in `IsSemilattice` (#2211)
Merge v2.1.1 into `master` (#2473)