Email Gateway (Aug 19 2022 at 15:00): Email Gateway (Aug 19 2022 at 15:00):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
With Isabelle2014-RC1 approaching, I would like to revive this questions
as I am also, so to speak, a »stake holder« of the theories where this
problem occurs.
So,
a) is this a deliberate change? (There is however no entry containing
»lift« in the NEWS).
b) if not, what shall we do about it? Someone must put on the helmet
and dig into to investigate,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 15:00):From: Ondřej Kunčar <kuncar@in.tum.de>
I'll do it.
Email Gateway (Aug 19 2022 at 15:03):From: Ondřej Kunčar <kuncar@in.tum.de>
Was addressed in b590fcd03a4a. Andreas, please, double-check that it
works for you. I tested it only on your minimal example.
Ondrej
Email Gateway (Aug 19 2022 at 15:04):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Ondrej,
Thanks. It also works in my real case.
Best,
Andreas
Email Gateway (Aug 19 2022 at 15:13):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
In Isabelle2014-RC0, lift_definition sometimes forgets that the setup_lifting declaration
has been given the (no_code) option. When that happens, I get bogus code equations in the
code generator setup which break the value command, because even NBE then complains about
sort constraints being violated. Below is an example that works in Isabelle2013-2, but not
in Isabelle2014-RC0. Of course, I can manually delete the code equations, but it would be
nicer if lift_definition could just stick to what setup_lifting has been told.
theory Scratch imports "~~/src/HOL/Main" begin
typedef ('a, 'b) foo = "{f :: 'a ⇒ 'b. ∀x. f x = undefined}" sorry
setup_lifting (no_code) type_definition_foo
lift_definition make :: "('a ⇒ 'b) ⇒ ('a, 'b) foo"
is "λg. if ∀x. g x = undefined then g else (λ_. undefined)" sorry
definition bar where "bar = make (λx :: nat. 0 :: nat)"
value "bar"
(* evaluates in Isabelle2013-2 to "make (λu. 0)",
but raises the following error message in Isabelle2014-RC0:
Wellsortedness error
(in code equation bar ≡ make (λx. zero_nat_inst.zero_nat),
with dependency "Pure.dummy_pattern" -> "bar"):
Type nat not of sort enum
No type arity nat :: enum
*)
Best,
Andreas
Last updated: Apr 20 2024 at 04:19 UTC