[isabelle-dev] BNF: number of dead variables
Christian Sternagel
c.sternagel at gmail.com
Wed Dec 3 15:01:12 CET 2014
Dear BNF gurus,
is there a reliable way to check - given the name of a type constructor
- how many dead type parameters it has?
I tried
(case BNF_FP_Def_Sugar.fp_sugar_of lthy tname of
SOME sugar =>
if BNF_Def.dead_of_bnf (#fp_bnf sugar) > 0 then
error "..."
...
However having something like
datatype foo = Foo | Bar
I noticed that
print_bnfs
does not list type "foo", what is worse, the above check apparently
yields a number greater than 0 for "foo", since the corresponding error
is triggered.
cheers
chris
More information about the isabelle-dev
mailing list