Re: [isabelle] Using counter example finder and 'a-types
But it is supported: try "rev xs = xs".
Moa Johansson schrieb:
I'd like to use Isabelle's counter-example finder, but unfortunately
often on conjectures with polymorphic types (eg. 'a list), which is not
supported as far as I know. Does anyone have any tips or hacks to work
around this, such as pretending the 'a list is a list of integers or
something like that?
This archive was generated by a fusion of
Pipermail (Mailman edition) and