Package for bridge to gaia #56
Merged
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
The Bridge branch should contains lemmas relating Gaia'a and Hydra-battle's T1 data-types (ordinals in Cantor normal form), both descendents of the old Cantor contrib.
|
@palmskog I fixed the conflicts in my (local )branch Bridge. So, the procedure is now to commit, then push Bridge ? |
|
@Casteran yes, if you fixed the conflicts on top of my (unrelated) changes, all you need to do is to commit locally and push to the upstream (GitHub) |
|
OK, For the time being, I'm writing in a strange cocktail of vanilla Coq and SSreflect, but I hope I'll improve the consistency of my scripts soon ... |
|
Well, I think SSreflect is fine. Since I’m a beginner, my first scripts in Bridge will have several old-fashioned features.
In Bordeaux, our Coq working-group want also to learn Ssreflect (since there are librairies they want to use).
I find it very interesting to build a bridge between a plain Coq library and a Mathcomp development.
Just one point: I’ll use the ‘ Set Bullet Behavior "Strict Subproofs ». ‘ option (compatible with SSreflects) which really helps me do structure my proofs.
… Le 14 août 2021 à 19:07, Karl Palmskog ***@***.***> a écrit :
@Casteran <https://github.com/Casteran> feel free to roll back my SSReflect proof changes if you want. Also, recall that you can get lia and nia to work with MathComp operators if you install the package coq-mathcomp-zify, and do after the usual MathComp requires:
From mathcomp Require Import zify.
See an example <https://github.com/math-comp/mczify/blob/master/examples/divmod.v>.
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub <#56 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AJW6FCQKUZVX2E7523RXIUDT42PEZANCNFSM5CFFUSTA>.
Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email>.
|
palmskog
commented
Aug 14, 2021
Co-authored-by: Karl Palmskog <palmskog@gmail.com>
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.
As per discussion in #55, I have added the package
coq-gaia-hydrasbased on Dune in this branch created by @Casteran. However, this branch is currently in conflict withmasterdue to changes previous to my commits in the regular ordinals part that are unrelated to the gaia proofs or packaging.Since I'm not sure how to proceed to get the branch mergeable (e.g., rebase and fix conflicts or just cherry-pick the gaia work in another branch?) I'm opening this draft PR.