Lasse Letager Hansen

Results 42 comments of Lasse Letager Hansen

I have done yesterday this in a branch on my fork of hacspec (https://github.com/cmester0/hacspec/commit/29c368bed8c34816a3e8b37e81eafac4a5e920c1), so I will have a look tomorrow.

It might be how I construct the `top_ctx` map (in `main.rs`), however I would expect it to work for constants, if it works for functions and types. Otherwise I would...

There does not seem to be any code in the `language` crate related to `hacspec_unsafe`, so it only does something when running as part of rust code, not when exporting...

The code development should be more or less done now, so I will start doing code cleanup, documentation, and CI.

Rebase master done, this just need some minor updates, then it should be done. We should probably also add this to the CI.

I had done almost the same as in #300 , so I have now updated to use CarrierTyp, instead of the updated version of EarlyReturnTyp (the two were equal). Also...

Yes, I also think it probably needs to be split.

I have things in a working state, so I will start splitting this in smaller PRs.

Oh, sorry I have not been to active on git lately. It seems `syn` version is not restricted (should be something like `1.0.101`) in the pearlite package, making it install...

Updating the Jasmin files seems a bit harder, than updating to mathcomp2 (and coq-8.18), as things have been moved around and renamed, and I do not have much knowledge about...