[isabelle] Type translation with a type variable



Greetings,

When I declare:

types 'a pptr = "(addr,'a) pptr_t"

how can I make that a print translation?

I want this to work:

translations
  "'a pptr" <=(type) "(32 word,'a) pptr_t"

but it won't let me. I can do this:

translations
  "pptr" <=(type) "(32 word,'a) pptr_t"

but that's no good, as "'a pptr" and "(32 word) pptr" will look the same.

Any advice?

Sincerely,

Rafal Kolanski.









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