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



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

On 10/21/2013 02:09 PM, Andreas Lochbihler wrote:
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






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