[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