[isabelle] Type translation with a type variable
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