Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Theory merge in wrong order leads to error in ...

Email Gateway (Aug 22 2022 at 15:04):

From: Lars Hupel <hupel@in.tum.de>
Dear list,

assume you have two files:

theory A
imports Pure
begin (* empty *) end

theory B
imports A Main
begin

datatype 'a test = Test

end

The "datatype" command produces a tactic failure, with the exception
"Congruence not a meta-equality".

If I swap the order of imports, the problem goes away.

I'm aware that changing the order of imports might influence qualified
names, but I haven't observed anything like that before. The above
example throws an error in 2016-1 (and 49c537d87896), but succeeds in
Isabelle2016.

Cheers
Lars

Last updated: Nov 21 2024 at 12:39 UTC