Maximilian Spitz (Jun 29 2023 at 07:57): 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 itselfyou 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 'ayou 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_offunction 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: Apr 27 2024 at 20:14 UTC