Lists

Stream: Is there code for X?

[Topologic]

I'm trying to get a sense of the built in methods associated to the list type. I know the basic stack methods for it.

• concatenate is ++
• (a :: l) is push

Now, do the following operations need to be defined by hand?

• delete the ith entry
• add in x : T in the ith entry
• get the ith entry
• splice the list
• length of the list

[Jason Rute]

I'm assuming you mean Lean 3. If so, you can enter list. in the mathlib docs and lots will come up, much of it in init.data.list.basic which should be available automatically without imports. Edit: There are more definitions in data.list.defs (which you will need mathlib for).

[Jason Rute]

If Lean 4, then you can enter List. into Lean 4 and you should get an autocomplete with many functions. Or look at the code in src/Init/Data/List

[Jason Rute]

And I think you will find that all the operations you want are already defined or can be done in a standard way with other operations (especially in Lean 3 + mathlib).

[Jason Rute]

It might also help to mention your use case. Operations on the "ith" element will be linear in i. If you are using this for mathematical theorems it doesn't matter, but if you are using them for computing (say meta-programming in Lean 3 or regular programming in Lean 4), it could add up. If you plan to iterate over all the elements in the list, then operations like list.map and list.foldl are good choices (or just plain recursion) even in mathematical definitions and theorems.