Support for weak cbv #18190
Merged
Support for weak cbv #18190
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
herbelin
added
kind: enhancement
coqbot-app
bot
added
the
needs: full CI
herbelin
added
the
request: full CI
herbelin
force-pushed
the
master+weak-cbv
branch
from
2423de9
to
6dc3c75
Compare
coqbot-app
bot
removed
request: full CI
|
Binding of weak cbv to reduction strategy Ideally, more tests could be done though [Added: done]. |
herbelin
force-pushed
the
master+weak-cbv
branch
from
6dc3c75
to
710fdb0
Compare
coqbot-app
bot
added
the
needs: full CI
This was referenced Oct 27, 2023
herbelin
added
the
request: full CI
herbelin
force-pushed
the
master+weak-cbv
branch
from
710fdb0
to
30a61da
Compare
coqbot-app
bot
removed
request: full CI
herbelin
added
the
request: full CI
herbelin
force-pushed
the
master+weak-cbv
branch
from
30a61da
to
b37c09c
Compare
coqbot-app
bot
removed
the
request: full CI
|
The job library:ci-fiat_crypto_legacy has failed in allow failure mode |
SkySkimmer
reviewed
Oct 30, 2023
SkySkimmer
approved these changes
Nov 7, 2023
SkySkimmer
added
the
needs: rebase
We block under lam, fix and the return clause and branches of match. However free variables are considered as constructors, i.e. we reduce "x t" info "x t'" where t' is the whd of t.
Include some rephrasing in doc, co-authored by Jim. Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
herbelin
force-pushed
the
master+weak-cbv
branch
from
b37c09c
to
82a9037
Compare
coqbot-app
bot
added
needs: full CI
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
|
@coqbot merge now |
|
@SkySkimmer: Please take care of the following overlays:
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is a variant of @maximedenes' weak-cbv branch providing a weak cbv strategy of reduction of the CIC call-by-name theory. In there, free variables are considered as "constructors", so that
x tevaluates tox t'wheret'is the weak-head normal form oft.It should be useful for #17503 (give access to the "weak" form of reduction strategies).
Updated test-suite
Updated changelog (originally from Add head reduction flags (
lazy head betaetc) #17503)Overlays: Adapt to coq PR #18190 adding a whd form of the cbv reduction strategy LPCIC/coq-elpi#528 and Adapt to coq PR #18190 adding a whd form of the cbv reduction strategy mattam82/Coq-Equations#566