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:

translations
   "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".

Sincerely,

Rafal Kolanski.


Rafal Kolanski wrote:
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.