Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Getting an induction theorem from a type-name ...

view this post on Zulip Email Gateway (Aug 22 2022 at 11:43):

From: Lucas Dixon <lucas.dixon@gmail.com>
Hi,

I'm trying to update and clean up some old IsaPlanner code (last updated
long before the new datatype package!).

I used to use something like this Datatype.get_info some_datatype_name.
But I want to move to using the new datatype package, and so
Old_Datatype_Data.get_info some_datatype_name will now return NONE.

So, what's the best way, in an ML function, given a string value for a
type-name (found by examining the underlying term's free variables) to
lookup an induction theorem that the datatype package generated? (where
should I look for an ML interface for working with the new datatype
package?)

Thanks!
lucas

view this post on Zulip Email Gateway (Aug 22 2022 at 11:43):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Lucas,

see the recent thread (https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-September/msg00180.html) where basically the same question has been answered already.

Hope that helps,
Dmitriy

view this post on Zulip Email Gateway (Aug 22 2022 at 11:44):

From: Lucas Dixon <lucas.dixon@gmail.com>
Thanks! Moa emailed me too, that was exactly what I was looking for. cheers!

Last updated: Apr 26 2024 at 08:19 UTC