Théophile Wallez
Théophile Wallez
A minimization inspired by guido (https://github.com/FStarLang/FStar/issues/3309#issuecomment-2165639699) ```fstar type rec1 = { x:int; } type rec2 = { x:int; } val bind : #a:Type -> #b:Type -> a -> (a ->...
@mtzguido following the depreciation of `FStar.Tactics.V1` (#3924) I ported Comparse to `FStar.Tactics.V2`. The last issue I face is that Comparse generates lemmas with SMT patterns, which do not work with...
Yes this solves it, thanks!
Further minimized to ```fstar let prim_arith_ty (p: unit): Type0 = let () = p in int -> int -> int let prim_arith_sem (p: unit): (prim_arith_ty p) = fun x y...
There is still something weird happening: ```fstar //let f (x:int) (y:nonzero): int = x / y let g (x:int) (y:nonzero): int = x + y let prim_arith_ty (p: unit): Type0...