agda-stdlib icon indicating copy to clipboard operation
agda-stdlib copied to clipboard

Published 20 hours ago • verified publisher icon agda

[ fix #1354 ] Refactoring Permutation.Propositional

Open gallais opened this issue 2 years ago • 4 comments

Still missing: CHANGELOG entries

gallais avatar May 03 '22 19:05 gallais

Closing as we've decided that its better to wait for typed pattern synonyms to finally make an appearance.

MatthewDaggitt avatar Sep 17 '22 13:09 MatthewDaggitt

Suggest re-opening this, as I seem to have got it to work with the pattern synonyms... using some ideas from #2317 and #2321 towards further unification, if someone can help me unify the two Permutation.*.Properties modules along the lines considered in #2317 ... incoming revised/streamlined/refactored/rebased commits shortly.

UPDATED: as with that more recent PR, will convert to DRAFT for now until ready to review.

jamesmckinna avatar Mar 17 '24 11:03 jamesmckinna

So far all the heavy lifting was done years ago by @gallais so props to him.

But I think that my recent work on #2317 hopefully points the way to getting the Properties unified as well. If that succeeds, then most of the guff in Propositional disappears entirely, and with it, all/most of the angst about qualified import of refl... I hope. Fingers crossed!

UPDATED Lots of refactoring work on #2317 ahead of bringing it to bear on this PR. But first see #2333 as a more manageable first part of a roadmap detailed there.

jamesmckinna avatar Mar 18 '24 07:03 jamesmckinna