Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Help on Nominal package


view this post on Zulip Email Gateway (Aug 17 2022 at 14:44):

From: Temesghen Kahsai <lememta@gmail.com>
Hi all
I just start to use the new Nominal package. And I get the following
error when I try to execute one of the examples provided in the package.


*** Cyclic dependency of constants:
*** "nominal.perm"
*** The error(s) above occurred in definition "perm_set_def":
*** "pi \<bullet> X == {pi \<bullet> a |a. a : X}"
*** At command "defs" (line 26 of "/Users/lememta/Desktop/tesi di
laurea/nominal_pkg-0.03/nominal_pkg-0.03/nominal.thy").
*** Error.
* At command "theory".* Cyclic dependency of constants:


Can somebody please give me a hint to solve this problem?
Thanks in advance for the collaboration.
Cheers

view this post on Zulip Email Gateway (Aug 17 2022 at 14:44):

From: Makarius <makarius@sketis.net>
On Fri, 19 May 2006, Temesghen Kahsai wrote:

I just start to use the new Nominal package. And I get the following
error when I try to execute one of the examples provided in the package.

Please ask at the nominal mailing list -- see
http://isabelle.in.tum.de/nominal/


*** Cyclic dependency of constants:
*** "nominal.perm"


Can somebody please give me a hint to solve this problem?

This is an effect of ongoing internal changes in the current Isabelle
development snapshot. Try to avoid using unofficial snapshots unless
there are really urgent reasons. In any case, the Isabelle NEWS file and
CVS ChangeLog (http://isabelle.in.tum.de/devel/ChangeLog.gz) will provide
some clues of what has been going on in Isabelle development recently.

Makarius


Last updated: May 03 2024 at 12:27 UTC