Discrete Functions / Maps

Stream: Is there code for X?

[Daniele Pusceddu]

Hello all,
is there a library that implements discrete functions / maps?
In particular I would like to start from a 'bottom' function, undefined for all values, and incrementally add bindings to it.
I am aware of PFun but extending it for bindings (and proving the related theorems) proved difficult. I was wondering if there is something more specific. I am not using Option because I would like to use Finset.sum on the bindings for example.

[Eric Wieser]

I suspect it's not really what you want, but with import data.fin.vec_notation you can write ![] for the function with no outputs, and f = ![a, b, c] for the function with f 0 = a, f 1 = b, f 2 = c

[Daniele Pusceddu]

Thank you for the suggestion. Indeed vec_notation is not what I am looking for but it is good to know that it exists.
I have just found finsupp and it may be the closest thing to what I am looking for.

[Eric Wieser]

Fundamentally Lean does not let you create a function that is "undefined" anywhere

[Eric Wieser]

But indeed, if you replace "undefined" with "zero" then you can use finsupp

[Eric Wieser]

You can also use regular function types and docs#pi.single or docs#function.update