vfukala

Are there some closure features that already partially work (possibly somewhere on another branch)?

A minimized example. This program verifies (with default flags) despite the `prusti_assert!(false);`: ```rust use prusti_contracts::*; struct List { sz: usize } impl List { #[trusted] #[ensures(result.sz == 0)] fn new()...

Similarly, when I just open this file: ```coq Require Import LiveVerif.LiveVerifLib. *) " Qed. Derive f SuchThat (fun_correct! f) As f_ok. { } Qed. ``` , I immediately get this...

It seems that the tactic itself is (still) broken. It looks like when there is a `match` on a variable that isn't named `x`, `destauto` fails. I wouldn't expect the...

Interesting, thanks for the insight! It really worked for me on 8.18 (and also 8.17, identically). Like so ``` Welcome to Coq ...,(HEAD detached at V8.18.0) (f022d5d194cb42c2321ea91cecbcce703a9bcad3) Coq < Goal...