clean up component dependencies of lia #150
Conversation
andres-erbsen
force-pushed
the
early-lia
branch
18 times, most recently
from
5b5c1c9 to
8e7d182
Compare
proux01
left a comment
proux01
left a comment
There was a problem hiding this comment.
Sounds reasonable at first glance
| <dt> <a name="zarith"></a><b>ZArith</b>: | ||
| Binary encoding of integers. | ||
| This binary encoding was initially developped to enable effective | ||
| computations, compared to the unary encoding of nat. Proofs were then added | ||
| making the types usable for mathematical proofs, although this was not | ||
| the initial intent. If even-more efficient computations are needed, look | ||
| at the <a href="#primitive-int">primitive-int</a> package below for 63 bits machine arithmetic | ||
| or the coq-bignums package for arbitrary precision machine arithmetic. | ||
| Everything can be imported with From Stdlib Require Import ZArith. | ||
| Also contains the migromega tactic that can be loaded with | ||
| From Stdlib Require Import Lia. | ||
| Integer-arithmetic properties | ||
| </dt> |
There was a problem hiding this comment.
We probably don't want to loose that information
There was a problem hiding this comment.
Updated. Most of the information is now split between entries for integers and primitive-int. I put back more mention of proofs and the suggested Require Import here. I removed the historical note because it does not seem relevant and important enough to be on the front page.
andres-erbsen
force-pushed
the
early-lia
branch
3 times, most recently
from
ab28487 to
c0e6db0
Compare
|
I addressed the comments and rebased. I think this PR is likely to go stale again; please also make a decision about how to handle the remaining overlay. |
proux01
left a comment
proux01
left a comment
There was a problem hiding this comment.
Would have been better to have multiple meaningful commits than a huge one but well, now it's done.
| Rational numbers, including canonical (Qc) and non-canonical (Q) | ||
| constructions on top of binary <a href="#integers">Integers</a> as well as | ||
| basic theory. Alternative definitions are available in coq-mathcomp-algebra | ||
| (unary rat and theory) or coq-bignums (machine-integer construction) and |
There was a problem hiding this comment.
Not sure what unary means here?
There was a problem hiding this comment.
https://en.wikipedia.org/wiki/Unary_numeral_system, referring to how rat is constructed in mathcomp
There was a problem hiding this comment.
Maybe "based on unary nat"?
| <dt> <a name="qarith"></a><b>QArith</b>: | ||
| Rational numbers, including canonical (Qc) and non-canonical (Q) | ||
| constructions on top of binary <a href="#integers">Integers</a> as well as | ||
| basic theory. Alternative definitions are available in coq-mathcomp-algebra |
There was a problem hiding this comment.
Maybe
| basic theory. Alternative definitions are available in coq-mathcomp-algebra | |
| basic theory. A more convenient definition is available in coq-mathcomp-algebra |
(it's not like the three following things are pure alternatives of one another, but one is nice for proofs, the other to compute efficiently and the third thing can be used to refine proved things to computable things)
There was a problem hiding this comment.
We disagree about which is more convenient.
There was a problem hiding this comment.
Maybe "more convenient for proofs" or "more convenient for mathematical developments"?
IIUC, this is only VST. You can probably ask them to merge it once their CI confirms it's indeed backward compatible. |
|
I responded to comments, please take another look CI says |
|
I will deal with the bedrock2 overlay propagation. If you could poke VST (as the assignee), that'd be great. Thanks! |
2 participants
Uh oh!
There was an error while loading. Please reload this page.