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?

Moa Johansson

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.