Xia Li-yao

With this batch of methods I've reached the milestone of verifying 7/10 of the unsafe slice methods (the "easy" ones) from the verify-rust-std challenge.

My current understanding is that `const` declarations (top-level and associated), `const` generics and `const {...}` expressions are all pretty straightforward in MIR so they are easy to translate into program...

Complication: `const` definitions from the current crate are handled fine, but not those from dependencies, because our mir-to-fmir translation uses an `BodyWithBorrowckFacts` which comes from a `LocalDefId`. - Why do...

> Why is the goal always a program function? I am proposing to make it so in order to be able to call `get_N`. In particular, when we generate a...

There was a similar discussion here: https://github.com/gspia/fcf-containers/issues/15 In hindsight it might have been preferable to have the lifted operators by default (i.e., give them the normal names) so that we...

@barci2 if you're looking for something to do, this could be it. Rather than lifted operators, it actually seems better to export unlifted operators `(++) :: [a] -> [a] ->...

If you have `(+) :: Nat -> Nat -> Nat`, you write `1 + 2`. If you have `(+) :: Exp Nat -> Exp Nat -> Exp Nat`, you write...

Thanks for the report! I think that may be difficult to solve because of the dependency in `forall` statements. The way shrinking is integrated in properties is too simplistic. If...

Sadly this is a non-working part of the QuickChick library. The function generators in QuickChick are not usable because we use a mutable PRNG API after extraction. `CoArbitrary` relies on...

Does first running the command without `-i` avoid the "no such file ..." exception?