Re: [isabelle] Option case and pairs with the function package


I stumbled across a syntax problem for the option_case expressions:

However, when I use the function package, when I want to show syntaxtest'.simps, not (case s of None ...) is displayed, but option_case ... s.

This is because the function package eta-normalizes the right hand sides, which breaks the case syntax. Currently there is no easy fix for this, unfortunately.


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