Nico Lehmann

@sql-koala are there any updates on this. I'm interested and I could help with testing/development if you need help.

This is the code that does the ANFing https://github.com/flux-rs/flux/blob/main/flux-refineck/src/fixpoint_encoding.rs#L291. Some things are very specific to flux, but it should be easy to implement the same directly in fixpoint. However, I...

I'm also interested in this feature and I would like to hear about any progress. If you look at any popular css framework (bootstrap, bulma,..) the basic thing they offer...

> Why is this is even in the project?, one of the things that I hate about Go linter and ESLint is that they force you to have a code...

I came to report the same thing. Also Arch running gnome 3.16.1

The easiest way to support this is by opportunistically doing const eval during lifting here https://github.com/flux-rs/flux/blob/main/crates/flux-middle/src/fhir/lift.rs#L540 Handling more complicated cases like const generics is a bit more involved.

this is orthogonal to const generics, but I've been looking at it and it sounds doable. I want to implement it. I think this is going to be necessary for...

Did some digging. The reason for this is that in the signature of `index` (and `index_mut`) the type variable `T` (of items) appears in a bound so we don't generate...

A blocker for this is that we rely on this unsoundness to have index syntax for `RVec`. The impl is ```rust impl std::ops::Index for RVec { type Output = T;...

It's a blocker because `fn(&RVec[@n], usize{v : v < n}) -> &T` (the impl) is not a subtype of `fn(&RVec, usize) -> &T` (the trait). But when I wrote that...