| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
[ZToField] -> [F.of_Z]
[FieldToZ] -> [F.to_Z]
[Zmod.lem] -> [F.lem]
|
| |
|
|
|
|
|
|
|
|
|
|
| |
ModularArithmetic now uses Algebra lemmas in various places instead of
custom manual proofs. Similarly, Util.Decidable is used to state and
prove the relevant decidability results.
Backwards-incompatible changes:
F_some_lemma -> Zmod.some_lemma
Arguments ZToField _%Z _%Z : clear implicits.
inv_spec says inv x * x = 1, not x * inv x = 1
|
| |
|
|
| |
[Local Coercion :=] changed meanings. Use [Let] and [Local Coercion] for consistent behavior
|
| |
|
|
|
|
|
|
|
|
|
|
| |
The file coqprime/Coqprime/ListAux.v was importing List, which was confusing
machines on which mathclasses was also installed.
Using https://github.com/JasonGross/coq-tools
```bash
make -kj10
cd src
git ls-files "*.v" | xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto
```
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
|
|
- F has a human readable complete specification
- F is a parametric type, not a parametric module
- Different F instances can be disambiguated by type inference,
which is more conventient that notation scopes.
- F has significant support for non-prime moduli
- It should be relatively easy to port existing GF code to F.
Since the repository currently contains code referencing both F and GF,
it makes sense to keep the names different for now. Later, F may or may
not be renamed to GF.
|
Andres Erbsen
Jason Gross
Jade Philipoom