Re: [isabelle] Record field names and accessing other constants

Hi Yannick,

You can refer to all constants with their unique long name (unless access has been disabled explicitly with hide_const). In your example, you can refer to y introduced in the consts declaration as TheoryName.y where TheoryName is the name of the theory that contains the declaration. Side remark: Name hiding is not specific to the record package.


On 02/08/2013 08:53 PM, Yannick Duchêne (Hibou57) wrote:
A sample case:

     consts y :: bool
     consts z :: bool

     record u = x :: bool
     record v = x :: bool y :: bool

     term "(| u.x = y |)"
     term "(| v.x = y, v.y = y |)"

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