Email Gateway (Aug 17 2022 at 13:45): Email Gateway (Aug 17 2022 at 13:45):From: Norbert Schirmer <norbert.schirmer@web.de>
Hello Benny,
Your declaration of start_forest is to general. You definition only defines
"start_forest:: 'a pre_graph => 'a pre_graph set"
Maybe this is your problem?
Otherwise send me a concrete lemma which leads to a concrete error message, so
that I can give you a more concrete answer...
Norbert
Email Gateway (Aug 17 2022 at 13:45):From: Makarius <makarius@sketis.net>
As Norbert has pointed out already, there seems to be an oddity with the
types of your definition. Isabelle2004 produces the following message:
### Definition of GenTest.start_forest :: "'a pre_graph => 'a pre_graph set"
### is strictly less general than the declared type (see "GenTest.start_forest_def")
while Isabelle2005 rejects it outright.
Makarius
Last updated: May 03 2024 at 08:18 UTC