finsupp

Stream: general

[Kenny Lau]

I have a new idea: let's build finsupp using multiset

[Kenny Lau]

heh, ignore me, this won't work at all

[Kenny Lau]

Do we really ever need α →₀ β where β has no addition?

[Mario Carneiro]

I would say yes. There are various places I can think of where you want some kind of finite support but the range doesn't necessarily have a structure so much as a default value. The tape of a turing machine is like this