Antonin Reitz

Steel: issue with subcomp framing rule for return?

4

Hi, I noticed the following small bug while using Steel with selectors, that also affects Steel without selectors. It can be demonstrated with the following minimal example using a dummy...

Hi, I noticed the following bug while using Steel with selectors, that also affects Steel without selectors. It can be demonstrated with the following minimal example using a dummy structure...

When clauses within match block sometimes supported?

1

Hello, I noticed the following strange behavior: match clauses seem to be in some cases usable and not completely disabled. It can be demonstrated with the following minimal example. ```fstar...

Hello, I noticed the following bug while using Steel with selectors, that can be demonstrated with the following minimal example, which contains a simple workaround. ```fstar module Reqens open Steel.Memory...

Fix Nix build header: F* and krml versions empty

6

Use `fstar.exe --version` instead of `git rev-parse HEAD` in `$FSTAR_HOME` directory. Indeed, when building the F*+KaRaMeL toolchain in a Nix environment, `$FSTAR_HOME` does not point to a git repository. I...