Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Type translation with a type variable

view this post on Zulip Email Gateway (Aug 18 2022 at 12:35):

From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
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.

Last updated: May 03 2024 at 04:19 UTC