Skip to content

Add Properties of List actions on Bools#3005

Open
Taneb wants to merge 1 commit into
masterfrom
bool-listaction-props
Open

Add Properties of List actions on Bools#3005
Taneb wants to merge 1 commit into
masterfrom
bool-listaction-props

Conversation

@Taneb

@Taneb Taneb commented Jun 8, 2026

Copy link
Copy Markdown
Member

I'm not sure of the name for and-locate and or-locate, but they're the whole reason I ended up making this PR...

@jamesmckinna

Copy link
Copy Markdown
Collaborator

It looks as though I added a note to Data.Bool.ListAction suggesting it be refactored to make use of https://github.com/agda/agda-stdlib/blob/master/src/Data/List/Effectful/Foldable.agda but I no longer entirely remember what I had had in mind!

Would it be better to refactor this PR to make use of the properties defined there? And perhaps to do that prior refactoring?

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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants