Skip to content

add Permutation_filter - #305

Merged
andres-erbsen merged 2 commits into
rocq-prover:masterfrom
OwenConoly:perm_filter
Aug 31, 2026
Merged

add Permutation_filter#305
andres-erbsen merged 2 commits into
rocq-prover:masterfrom
OwenConoly:perm_filter

Conversation

@OwenConoly

Copy link
Copy Markdown
Contributor

Permutation_map, Permutation_flat_map, etc. already exist, but this one seems to have been forgotten.

Comment thread theories/Sorting/Permutation.v Outdated
Co-authored-by: Andres Erbsen <andres-github@andres.systems>
@andres-erbsen

Copy link
Copy Markdown
Collaborator

The Nix CI flocq install failure looks unrelated:

buildPhase completed in 1 minutes 21 seconds
Running phase: installPhase
Building install
mkdir: cannot create directory '/nix/store/ss49wyba13kmfx1iqqn8jab6ysgz8rd7-rocq-9.2.0/lib/coq/user-contrib/Flocq': Permission denied
Failed to build install
error: Cannot build '/nix/store/g2r6by5bz28zlvdcrbffaa3p0p49g0iq-coq9.2-flocq-dev.drv'.
       Reason: builder failed with exit code 1.
       Output paths:
         /nix/store/hisn77xzjqig6v82cgmq4w9945iw6ya9-coq9.2-flocq-dev

Merging.

@andres-erbsen
andres-erbsen merged commit 1593d61 into rocq-prover:master Aug 31, 2026
169 of 173 checks passed
@OwenConoly
OwenConoly deleted the perm_filter branch August 31, 2026 23:57
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