Re: [isabelle] Composing BNFs



> - in the below example, for the type "('a option + 'b ) list + 'c", a function "sum1.sum1.sum1.list.map_list_lift1_permute_201_01" is created. Can this be avoided / why is this needed, and why is a function created that ignores its last argument?

For my particular use case, that's not a problem. But I can't find the
definition of that constant, which means I can't unfold it. Is the
definition recorded somewhere?

Cheers
Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.