From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear BNF developers,
I just noticed that for the case combinator, the BNF package forgets to prove and register
the parametricity theorem as [transfer_rule] for datatypes without type variables. It only
proves and registers the one for the recursor. As the case combinator is also polymorphic,
it would be great if I had not state and prove the theorem manually.
Here's a minimal example:
datatype test = A nat | B bool
thm test.case_transfer (* does not exist *)
datatype 'a test2 = A nat | B bool
thm test2.case_transfer (* does exist *)
Best,
Andreas
Last updated: May 04 2024 at 04:19 UTC