notation for cardinalities

Stream: general

[Eric Rodriguez]

I'm planning to make a (localized?) notation for the cardinalities of sets and types, and I was thinking of using | and ‖ (kind of like what is currently used in card_embedding.lean. Does anyone have any objections to this, anything to watch out for? Should I make a notation class for either of these? Not sure whether they are used much elsewhere in Lean

[Yakov Pechersky]

We have this I think, docs#cardinal

[Yakov Pechersky]

And for finite types and sets, fintype.card and finset.card

[Yakov Pechersky]

Finally, for set cardinality where you want a regular old nat, docs#nat.card

[Eric Wieser]

Perhaps we could introduce #ᶠ for fintype.card since # is cardinal.mk?

[Eric Rodriguez]

that seems reasonable, and what about for finsets?

[Eric Rodriguez]

maybe #^s? (I can't find superscript s - does it exist?)

[Yakov Pechersky]

Why not just use projection notation for finset? Similarly, rename nat.card to set.card?

[Eric Rodriguez]

in my experience, it's been really annoying mixing up fintype and finset cards

[Eric Rodriguez]

this is why I liked the |set| and ‖type‖ idea but think the $\#^f$ seems reasonable for mathlib consistency

[Yakov Pechersky]

Can you share where they're confusing?

[Eric Rodriguez]

Most places where they have been I've made it local notation, but for example I've got a big proof in https://github.com/ericrbg/HatGames and that would be illegible without it I think, the .cards end up being sprinkled everywhere and ruining the flow