Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] 'a and 'a'

view this post on Zulip Email Gateway (Aug 22 2022 at 11:20):

From: "Roger H." <s57076@hotmail.com>
Hello,what is the difference between 'a and 'a' ? Can you give me an example?Thank you!

view this post on Zulip Email Gateway (Aug 22 2022 at 11:21):

From: Makarius <makarius@sketis.net>
Both are type variables, but of different name. The initial prime is
always required for type variables. More primes belong to the regular
identifier syntax of Isabelle, like x and x' for term variables.

Makarius

Last updated: Nov 21 2024 at 12:39 UTC