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
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