Re: [isabelle] BNFs and sort constraints
BNF type variables may not have sort constraints. "map_id" is part of
the BNF structure, so it accordingly doesn't have sort constraints.
More high-level theorems and constants are declared with the sort
constraints. To overgeneralize a bit, Dmitriy's low-level BNF code
doesn't like sort constraints, whereas my higher-level "(co)datatype"
code copes with them to the extent possible. In the code, you'll see
this by grepping for "unsorted_As" in "bnf_fp_def_sugar.ML".
that sounds basically like what I guessed from my observations. Thanks
for the clarification!
Incidentally, what is the motivation for your example? Is your
application related to item 5 in the "Known Bugs and Limitations" of
the "datatypes" document?
I don't intend to use this in any way. I'm merely trying to "tie up
My dictionary construction will just ignore sort constraints from data
constructors, and I was trying to figure out to what extent they might
be introduced in datatypes, e.g. by having a constrained BNF through
which recursion occurs.
The "meta-theorem" I am aiming for is that by dropping the sort
constraints you'll still end up with exactly the same datatype; i.e., I
want to argue that not supporting constraints in constructors is not a
problem because I can always ask the user to remove the constraints.
NB, because you mentioned "limitation 5": The fact that the overloaded 0
is a constructor for "nat" is the bane of my existence. It messes with
so many things and it is surprising that it works at all :-)
This archive was generated by a fusion of
Pipermail (Mailman edition) and