Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] uncaught exception from Isabelle 2009-2

view this post on Zulip Email Gateway (Aug 18 2022 at 16:04):

From: Randy Pollack <rpollack@inf.ed.ac.uk>
In Isabelle 2009-2:

theory bugSatoHS imports Nominal begin
atom_decl par
nominal_datatype trm1 = tpar par
and trm2 = atrm
nominal_primrec p1sub1 :: "trm1 => trm1 => par => trm1"
where
"p1sub1 (tpar p) t q = t"

*** exception Subscript raised (line 97 of "./basis/List.sml")
*** At command "nominal_primrec".

The problem seems to be that the "mutual" part of the primrec
definition for trm2 is missing.

Best,
Randy

Last updated: Apr 26 2024 at 16:20 UTC