[isabelle] Cardinality for infinite sets
- To: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Cardinality for infinite sets
- From: Diego Marmsoler <diego.marmsoler at tum.de>
- Date: Wed, 21 Mar 2018 18:19:24 +0000
- Accept-language: en-US
- Authentication-results: postout.lrz.de (amavisd-new); dkim=pass (2048-bit key) reason="pass (just generated, assumed good)" header.d=tum.de
- Thread-index: AQHTwUEkh92Kk5bYhEqjX1E3r9xe/w==
- Thread-topic: Cardinality for infinite sets
Dear Isabelle experts,
while playing around with "card" from theory Finite_Set, i recognized that it returns 0 for infinite sets.
Now i was wondering whether someone knows about a similar construct which, for this case, returns infinity from the extended natural numbers.
Many thanks in advance!
This archive was generated by a fusion of
Pipermail (Mailman edition) and