Clément Blaudeau
Clément Blaudeau
Still relevant. Fits into a greater effort to improve diagnostics and error messages.
Still very much relevant
This is especially useful for integration of Core-models (model of Rust core lib without unsupported-by-hax features)
The original issue is fixed. However, an empty loop without side effect will still throw an error : https://github.com/cryspen/hax/issues/405
Closing this as unplanned. The ergonomics should be better in the Rust engine.
Will be fixed when porting the importer to Rust (#1524)
It should be possible to have do-blocks in array-length expressions. Returns are forbidden (see https://doc.rust-lang.org/stable/error_codes/E0572.html)
Closing this issue as unplanned, as we focus on the Rust engine.
The same issue also appears in Lean. Such implicit parameters should be named differently in a (small) engine phase.
The workaround is to name the implicit parameters, turning ```rust fn f(arg1: impl Clone, arg2: impl Clone) {} ``` into ```rust fn f(arg1: T1, arg2: T2) {} ``` [Open this...