Skip to content

Refactor specs in unique_lock#47

Closed
dkxb wants to merge 10 commits intoSkyLabsAI:mainfrom
dkxb:unique-lock
Closed

Refactor specs in unique_lock#47
dkxb wants to merge 10 commits intoSkyLabsAI:mainfrom
dkxb:unique-lock

Conversation

@dkxb
Copy link
Copy Markdown
Collaborator

@dkxb dkxb commented Apr 20, 2026

No description provided.

@dkxb
Copy link
Copy Markdown
Collaborator Author

dkxb commented Apr 20, 2026

Should operator_bool_spec be defined on owns_lock_spec, since they have the same semantics?

Comment thread rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
@gmalecha-at-skylabs gmalecha-at-skylabs changed the base branch from unique-lock to main April 29, 2026 16:24
@pgiarrusso-sl
Copy link
Copy Markdown
Contributor

Our CI cannot support fork of our repos, so we'll use #51 instead.

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.

3 participants