Re: [isabelle] Qualified/Private with lifting package in Isabelle2015-RC4

Hi RenÃ,
the reason is probably that lift_definition uses Local_Theory.restore, which was an idiom how to achieve certain things before the new feature with limited name space accesses came out. There wasn't much time to port Lifting in this regard. We intend to do this for the next release. Notice that the same decision was made for datatype and co. by the BNF guys.


On 05/11/2015 08:58 AM, Thiemann, Rene wrote:
Dear all,

it seems that the modifiers qualified/private are just ignored by lifting.
As an example consider

theory Scratch
imports Main

typedef pos = "{n :: nat. n > 0}" by auto

setup_lifting type_definition_pos


private definition priv_nat :: "nat => nat" where
   "priv_nat x = x"

private lift_definition priv_pos :: "pos => pos" is
   "% x. x" .

qualified definition qual_nat :: "nat => nat" where
   "qual_nat x = x"

qualified lift_definition qual_pos :: "pos => pos" is
   "% x. x" .

Then after closing the context,
- qual_nat is accessible only qualified: Scratch.qual_nat (as desired)
- priv_nat is not accessible (as desired)
- but priv_pos and qual_pos are both accessible without any qualifier (not as expected)

Best regards,

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