Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 18 2022 at 10:48):

From: Moa Johansson <s0199173@sms.ed.ac.uk>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 10:49):

From: Tobias Nipkow <nipkow@in.tum.de>
But it is supported: try "rev xs = xs".

Tobias

Moa Johansson schrieb:

Last updated: May 03 2024 at 04:19 UTC