Re: [isabelle] Type translation with a type variable [SOLVED]
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 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and