Lucas Franceschino comments

Results 275 comments of


                                            Lucas Franceschino

Support patterns on arrays and opaque types.

I started to look at this a bit, there are issues with fresh vars I think https://hax-playground.cryspen.com/#fstar/7ec551634b/gist=898efdab8cc9c41469c5f28e72216b6e

Rewrite control flow inside loops.

Great, looking at it. Next PR can you resolve discussions that you think are handled?

Deep updates in F* blows up memory.

This was partially fixed in F* by https://github.com/FStarLang/FStar/pull/3861, though we need to use the special flag `--ext optimize_let_vc`. Also, there is https://github.com/FStarLang/FStar/pull/3970 which is improving the situation, but not merged...

Needs Design: Allow &mut and raw pointer returning functions in interfaces

Still relevant

Additions to proof-libs needed for the GCD example

On the F* side, you could define: ``` val trailing_zeros: #t:inttype -> int_t t -> (n:u32{v n >= 0 /\ v n

`..` patterns in matches should throw an error

Still relevant

Empty clauses in match generate syntactically ill-formed code in F*

This is still relevant

Missing OPAM flag on installation instructions when working with several switches

Where does the dependency of `topkg` comes from? If we can indeed drop it that's great. (I'm not using opam myself, so I'm not seeing those problems :S)

Missing OPAM flag on installation instructions when working with several switches

I recall we discussed that informally, @clementblaudeau do you recall what was the conclusion here?

[rengine]: Missing support for fresh modules

Fresh modules are used by the phase that inserts bundles; those are useful in backends in which two mutually dependent items must live in the same namespace. This is not...