Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Plugin gets executed twice

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

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

I'm trying to import my AFP entry "Constructor_Funs" along with other
theories and I've noticed some odd warning upon theory merge. This can
be reproduced with:

theory Scratch
imports
"$AFP/Coinductive/Coinductive_Nat"
"$AFP/Constructor_Funs/Constructor_Funs"
begin

The warning says "enat already processed" and is generated by my code
when it is invoked a second time on the same type. I'm not sure why this
is happening; certainly it shouldn't happen on theory merge.

Cheers
Lars

Last updated: Apr 18 2024 at 08:19 UTC