Lasse Letager Hansen

Add match guard to AST

2

I have added the match guard to the AST. Currently no backend supports these, so this makes the rejection of this feature explicit. Furthermore we can now add a phase...

Coq proof lib

11

Add coq library files.

Incorrect order for Deps.sort

4

The following piece of code ```rust pub trait Foo { const c : u32; } pub struct foo {} impl Foo for foo { const c : u32 = 17;...

We could add a deep embedding of Hacspec, this would enable us to reason cross backend, and allow us to make the semantics of Hacspec precise. An attempt at defining...

Document valid CFG for Hax

1

Generate the accepted Hax syntax using a shallow printer.

Coq generic printer

1

Transition coq to using the Generic printer.

Mutable Variable and Function analysis are using String instead of Concrete Ident

1

This is an issue with #348 . Using `concrete ident` for functions in traits result in the identifiers not being equal. We need to have some way of testing if...

Should we move the running of coverage into the tests? We are not testing the extraction, just that the semantics are still valid. So the tests are different, but could...

Currently the Coq extraction uses TODO as the namespace for generated files. It should use the name of the crate instead, to be consistent with imports / multiple crate projects.