Re: [isabelle] Theory merge in wrong order leads to error in datatype



Hi Lars,

note that this is not specific to datatypes, but rather the general simplifier setup seems to be really messed up with this order of imports.

Try e.g.,

theory B
 imports A Main
begin
  
lemma "x = y â y = x"
  by simp (* Failed to apply initial proof method *)

fun f where (*Tactic failed*)
  "f x = x"

end

Dmitriy

> On 13 Feb 2017, at 17:09, Lars Hupel <hupel at in.tum.de> wrote:
> 
> 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
> 





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