Re: [isabelle] Combining BNF and Quotient

On 03/07/2013 12:58 PM, Makarius wrote:
On Thu, 7 Mar 2013, Ondřej Kunčar wrote:

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.

Can some of the quotient guys please clarify the situation.

How many quotient packages are there at the moment in Isabelle? Are
there plans to converge them, and remove old stuff?

I know that this is a lot of extra work, but this is how we usually
managed to keep things going (and moving forward) over so many years.


There is one Quotient package and there is Lifting and Transfer, which almost subsume the functionality of the Quotient package regarding defining new constants and transferring goals. When Lifting and Transfer subsume the Quotient package completely, the Quotient package will be probably outdated and eventually removed. Only the quotient_type command will be preserved. It's on my todo list but not really on the top because there are more important things to be done.

As far as I know, the only place where some extra features of the Quotient package (that are not covered by Lifting and Transfer) are used is Nominal2.


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