[isabelle] Interpretation problems of locales with datatype declarations
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Interpretation problems of locales with datatype declarations
- From: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
- Date: Tue, 3 Nov 2015 10:52:18 +0100
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0
Dear BNF experts,
I have started to use datatype declarations inside locales, but this seems to cause
problems at interpretations. Here is an example:
locale l = fixes n :: nat begin
datatype 'a foo = Foo 'a
interpretation l 0 .
The interpretation raises
exception THM 0 raised (line 1216 of "thm.ML"):
Type not of sort term_of
term_of_class.term_of ?x â ?t
If the interpretation is inside a proof (rather than at the top-level), interpret works
once, but I get a different error upon the second interpretation:
locale l2 = fixes b :: bool begin
datatype 'b bar = Bar | Foobar 'b
interpret t!: l2 True .
Here, interpret complains that
Monotocity rule for type "Scratch.l2.bar" is already_defined.
Is this a fundamental problem of the BNF package and locales or just a limitation of the
current implementation? Can I disable some plugins to make the examples work?
This archive was generated by a fusion of
Pipermail (Mailman edition) and