Clément Blaudeau comments

Results 48 comments of


                                            Clément Blaudeau

Support `PartialOrd` and other generated things

Will probably be addressed when porting the importer to rust

[Lean] Panic-freedom tutorial example is broken

Indeed! Thanks for the report. The bump of Lean version changed the syntax of pre/post conditions, which broke the example. I'll fix it asap. And, indeed, we should try to...

Recursive functors cannot be defined using module aliases

(side note) You cannot technically get an alias to `F` within the definition of `F`, as aliases to other recursive modules -- within the recursive knot -- are disallowed (which...

Wrong pattern at call site with 2 `&mut` parameters

Probably introduced by `And_Mut_defsite`. Will be fixed in the re-implementation in rust. (Keeping the issue open until then)

Cyclic dependency between trait definitions doesn't work well with F*

Still relevant

Engine crashes on refinement types with wildcard as binder

We should have a proper error message or a fix.

Missing f* files for nat_mod_macro

Is it still needed @matthiasspielberg1 ? For now, we're closing it as unplanned, but feel free to reopen the issue.

Proof libs: `%` is modeled as an euclidian remainder while it's just a remainder

I've noticed it while working on the Lean backend, where `%` has the same semantic as Rust. This breaks the spec of Barrett for instance : ```rust #[hax_lib::fstar::options("--z3rlimit 100")] #[hax::requires((i64::from(value)...