Re: [isabelle] Type translation with a type variable [SOLVED]

Hi Everyone,

I managed to solve this eventually by grepping through the HOL theories (couldn't figure it out from the docs).

So for anyone googling "translations type variable" the solution is:

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

(note the "a" is on the right despite eventually being printed on the left)
This will cause:

typ "(32 word, nat) pptr_t"

to be printed as "nat pptr".


Rafal Kolanski.

Rafal Kolanski wrote:

When I declare:

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

how can I make that a print translation?

I want this to work:

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

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

  "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?


Rafal Kolanski.

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