Clément Blaudeau
Clément Blaudeau
Currently, the lean backend outputs everything in a single file. It should split, probably based on modules. Splitting in several files may require to support alias items (indirections from outside...
Lean name rendering always returns fully qualified names, even in the file that defines them. Instead, we should strip names of the prefix of the current file. For instance ([in...
As all rust computation is happening within a `do` block, we could use Lean `for` loops instead of translating them to Hax folds.