Lucas Franceschino comments

Results 275 comments of


                                            Lucas Franceschino

Supporting the `Iterator` trait

Thanks for the bug report! Things are indeed a bit rough on the edges around iterators. We won't have time this week to take a look, but we will try...

Use ghost state

### Rust variable bindings is what we want (I believe) As we discussed last week, the API you're describing @franziskuskiefer would not play nice with hax: - it is stateful,...

Leftover makefile improvements

Let's close

Extraction error with `const` generics and hax attribute on a struct field

Thanks for your bug report! That's indeed a bug related to constants and struct refinements, I recall stumbling upon it quite some time ago. From what I recall, the proc...

@karthikbhargavan and I inverstigated a bit this. Notes: - the indirection via the `values` field of `Coefficients` will probably makes us hit https://github.com/FStarLang/FStar/issues/3800 to a certain degree. Would be much...

Cannot access previous struct fields in `refine` attributes

Sorry, I missed this issue somehow. Indeed, the refinements on the fields have an order constraint: in F*, having a refinement on a field that mentions another field that comes...

Cannot access previous struct fields in `refine` attributes

I'm taking a look at that right now. My strategy is: - cryspen/hax-evit#34 - cryspen/hax-evit#35

feat(docs): CONTRIBUTING.md: add guidelines for hax

Sounds good to me, thank you!

Stack overflow for deep expressions in bincode serialization/deserialization

I think we should bisect here, to understand exactly what went wrong and when

Stack overflow for deep expressions in bincode serialization/deserialization

Yeah, we wanted to use stacker as well, thanks for the tip! :) But there are a number of odd things around this bug, we need to understand exactly what's...