Isabelle/HOL back-end does not support Why3 arrays
The use of the Why3 library array.Array
triggers an error in the generated Isabelle/HOL output, say on examples/zeros.mlw
:
Malformed global fact "zeros_SetZeros_set_zerosqtvc_1.set_zerosqtvc.facts.mixfix_lblsmnrbqtspec(1)"⌂
Illegal fixed variable: "'a"
This might be a more general error triggered by the use of polymorphic types.