## Stream: new members

### Topic: defining a map out of a list

#### Dean Young (May 03 2023 at 18:33):

How do I inductively define a map out of a list?

def sum_the_elements  : (sequence : List Int)  Int :=
match sequence with
| a ++ [s] => (sum_the_elements a) + s

#### Dean Young (May 03 2023 at 18:34):

I want to modify the example to produce a function which sums the elements.

#### Henrik Böving (May 03 2023 at 18:35):

is there a particular rreason you are not matching on nil and cons but instead on append?

#### Kyle Miller (May 03 2023 at 18:36):

docs4#List.sum will sum the elements of a list.

#### Kyle Miller (May 03 2023 at 18:38):

Notice that List.foldl in its definition is a way to recurse where the last element is summed last.

#### Dean Young (May 03 2023 at 18:48):

@Henrik Böving for my purposes I want something that appends at the end of the list and not the beginning.

#### Henrik Böving (May 03 2023 at 18:48):

Right but why is that relevant to yourr sum function? It is commutative anyways

#### Dean Young (May 03 2023 at 18:52):

I was just interested in learning how it works I think.

But I can't even seem to get this to work:

def j (l : List Int) : Int :=
match l with
| cons fdfd fdfd2 => (j fdfd2) + fdfd
| nil => 0

lean seems to think that fdfd is a proposition.

#### Dean Young (May 03 2023 at 18:59):

def append (as bs : List α) : List α :=
match as with
| nil       => bs
| cons a as => cons a (append as bs)

this example is taken from the tutorial, but my lean thinks that nil is supposed to be a proposition.

#### Dean Young (May 03 2023 at 18:59):

this is lean 4 by the way

#### Henrik Böving (May 03 2023 at 18:59):

No, the issue with your code is that cons and nil are not top leve identifiers so you have to do one of List.cons .cons (note the dot) fdfd :: fdfd2 and [] or open the List namespace which is most likely what happened in the example

#### Henrik Böving (May 03 2023 at 19:00):

Kind Bubble said:

this is lean 4 by the way

I know^^

#### Dean Young (May 03 2023 at 19:04):

Is opening the List namespace recommendable? Does that just tell Lean to use the terminology from the list section of documentation?

#### Henrik Böving (May 03 2023 at 19:07):

So, there are actually two ways of opening the List name space, you can open List which basically takes all identifiers frrom the List namespace and makes them directly accessible or you can use

namespace List

def function...

end List

which actually adds function to the List namespace so you can later do List.function or even use xs.function where xs is a List. The second is (obviously) interesting if you wish to extend the functions directly available on List. The first is interesting if you want to just use functionality from a namespace. However given the fact that you can even use the [] and :: syntax to match on a list I see no reason to do the open List thing. I would usually use it when for example writing a Lean metaproogramm to open Lean so you don't have to prefix literally every line with Lean.

#### Dean Young (May 03 2023 at 19:33):

I think it has another issue though,

inductive jkljkl (α : Type) where
| nil  : jkljkl α
| cons : α  jkljkl α  jkljkl α

gives me

Main.lean:44:9: error: type expected
failed to synthesize instance
CoeSort (?m.6367 = ?m.6392) ?m.6398
Main.lean:45:7: error: expected command

#### Eric Wieser (May 03 2023 at 19:35):

You've only shown us three lines, and your error is on line 44

#### Eric Wieser (May 03 2023 at 19:35):

Can you make a #mwe?

#### Dean Young (May 03 2023 at 19:38):

notation p "|" q => transitivity p q

which is no good!

#### Eric Wieser (May 03 2023 at 19:38):

If you're not familiar yet with Lean 4's regular syntax, I would strongly recommend against defining your own syntax that remotely resembles something that is builtin

#### Dean Young (May 03 2023 at 19:40):

Ok -- and thanks for your help.
@Henrik Böving thanks!

Last updated: Dec 20 2023 at 11:08 UTC