Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2013-1-RC3: setup_lifting raises TYPE


view this post on Zulip Email Gateway (Aug 19 2022 at 12:10):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
When I try to setup lifting for a generic type copy using setup_lifting, I get an
exception TYPE. Here's a minimal example:

theory Copy imports Main begin
typedef 'a copy = "UNIV :: 'a set" ..
setup_lifting type_definition_copy
end

Is this on purpose (then I would expect a sensible error message) or a limitation?

Andreas

view this post on Zulip Email Gateway (Aug 19 2022 at 12:10):

From: Ondřej Kunčar <kuncar@in.tum.de>
Your raw type is 'a in this example. The setup_lifting doesn't support
type variables as raw types. You are right; the error message should be
better.

Ondrej


Last updated: Mar 28 2024 at 16:17 UTC