Re: [isabelle] Combining BNF and Quotient
Hi Ondřej and Jasmin,
thanks for the feedback.
On 07/03/13 09:31, Ondřej Kunčar wrote:> On 03/07/2013 08:32 AM,
> You can setup the Lifting package manually even for quotient types.
> Again by setup_lifting by providing the Quotient theorem (and
> optionally reflp theorem). See the documentation in The Isabelle/Isar
> Reference Manual. An example is in Word.thy. The command
> setup_lifting is not only for typedefs.
I think I will go that route, then. Proving a quotient theorems seems
less work than proving the necessary theorems for the BNF package.
> If you mean the Quotient package by Kaliszyk, Urban, I think you
> would have to go to the ML level (which doesn't exist, I know ;)) to
> setup the package manually.
So far, Coinductive used this very Quotient package, but I guess I can
transfer everything to the lifting/transfer package, as the BNF package
already constructs the type.
This archive was generated by a fusion of
Pipermail (Mailman edition) and