Re: [isabelle] Using counter example finder and 'a-types



But it is supported: try "rev xs = xs".

Tobias

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?

Cheers,
Moa Johansson





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