Re: [isabelle] primcorec does not terminate

> When I use primcorec, I usually either define it using the destructor view (and then manually derive a suitable code view -- the automatically generated one is usually not idiomatic) or specify the code view with cases (from which I derive pattern-matching equations using simps_of_case) and then manually derive the destructor rules, as the generated theorems use cases rather than selectors and discriminators.

Using selectors and discriminators for these is also on my TODO list.


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