Lasse Letager Hansen
Lasse Letager Hansen
Fixed an ordering issue in #231
Seems that fstar and easycrypt does not have full coverage of the examples, so I am gonna just generate the examples for Coq for now.
I cannot get the CI to push the updated files, since the pull request originates from a fork. So for now I will just generate the files, and try and...
This should be ready for review, however it only tests that the files can be updated, but does not actually commit / push the updates. I restructured the crates, so...
@franziskuskiefer do we want to add anything to this? Or should we just get it reviewed and merged?
It seems like there is some issues with resolving conflicting function/method names on the public_nat_mod types (eg. the inv function). This results in different number of arguments being expected between...
I had the same issue with the coq backend, you can have a look there for a possible fix, since the code was copied from the fstar implementation to begin...
A similar issue occurs if you do not `use hacspec_lib::*;` for ```rust pub fn bar() { Option::::None; } ```
Some students just encountered this issue again and was confused. They wanted to pattern match on an index of a Seq of tuples, however got an error stating that the...
Should there be implementations in the backends for `big_integers` and `vec_integers_*` ? Currently that is the main part of the coq library missing functions.