[isabelle] Composing BNFs
Dear BNF experts,
I'm looking for a simple way to obtain a composed map function given a type.
For example, given
('a + 'b) option list
the result should be a term of type
('a â 'c) â ('b â 'd) â ('a + 'b) option list â ('c + 'd) option list
It doesn't necessarily need to be a constant; instead, it could be a
simple term composition of map functions.
I found "BNF_Comp.bnf_of_typ" but I'm a little confused about all the
parameters it takes. Is there a small, canonical example somewhere?
Also, can I get "bnf_of_typ" (or something else in BNF) to produce a
bunch of terms instead of constants, typedefs and everything?
This archive was generated by a fusion of
Pipermail (Mailman edition) and