[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 MHonArc.