## Stream: Beginner Questions

### Topic: Type cardinality

#### Maximilian Spitz (Jun 29 2023 at 07:57):

Hi, I have a function f, which takes a type parameter `'a itself => ... => ('a::finite)` and in a proof of the form `f t ... = ...` I want to access the cardinality of t `CARD('a)` in the sense of `CARD(t)`, but that does not work. I suspect there might be a function like `itself_card t`, but I could find nothing.

#### Simon Roßkopf (Jun 29 2023 at 08:09):

Hi,

could you describe what you mean by "cardinality of t"? If you want the cardinality of the set of all elements of type `'a itself`you could get it by using `card (UNIV :: 'a itself set)`, but I think this is unspecified(iirc itself is just there so the embedding of types into terms has one canonical representative `TYPE('a)` and nothing else is specified). If you want the cardinality of the set of elements of type `'a`you can use ``card (UNIV :: 'a set)`

#### Maximilian Spitz (Jun 29 2023 at 08:14):

Thank you, I should clarify: I have a function with a type variable, which is constrained as enum, so a type with finitely many instances. In the function definition I have access to 'a, but not in the proof. In the proof I have only t, which has type 'a itself and from t I want to get CARD('a) somehow, but I cannot access it directly. In short: I cannot mention 'a in the proof

#### Manuel Eberl (Jun 29 2023 at 08:33):

I still don't really understand the problem. You should be able to access that type variable in the proof. But it's hard to say without having a concrete example.

But if you want you can define a `card_of` function yourself, e.g. as an input abbreviation:

``````abbreviation (input) card_of :: "'a ⇒ nat" where
"card_of _ ≡ card (UNIV :: 'a set)"
``````

(or something like that; not sure what a good name would be)

#### Maximilian Spitz (Jun 29 2023 at 08:54):

Manuel Eberl said:

I still don't really understand the problem. You should be able to access that type variable in the proof. But it's hard to say without having a concrete example.

But if you want you can define a `card_of` function yourself, e.g. as an input abbreviation:

``````abbreviation (input) card_of :: "'a ⇒ nat" where
"card_of _ ≡ card (UNIV :: 'a set)"
``````

(or something like that; not sure what a good name would be)

Thank you, that works fine.

Last updated: Sep 11 2024 at 16:22 UTC