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.

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)`

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

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)

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: Feb 27 2024 at 08:17 UTC