missing encoding of polymorphism
On the following, a call to a prover requiring polymorphism to be encoded fails:
goal G0: (fun x -> x) 0 = 0For instance:
> why3 prove -P cvc4 test.mlw
This type isn't supported:
'a -> 'a
smtv2: you must encode type polymorphism
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information