Stream: Archive Mirror: Isabelle Users Mailing List

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

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

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

Last updated: May 03 2024 at 12:27 UTC