Understanding arrays, and option types.

Stream: new members

[Debangan Mishra]

I am very new to lean, and want to learn how to use arrays and lists. The following is my implementation for extracting the maximum value from the list of numbers. However, when I use the inbuilt function list.maximum, I get 'some \N' and not just a natural number. What is the intuition behind that? And also, as the list is immutable, I cannot modify the original list, so I have to get a new list, which I am not comfortable with. What to do in this case? I want to use this as a starting point for constructing heap data structure in Lean.

import data.list.basic

def convert_to_nat (value : option ℕ) : ℕ :=
  match value with
  | none := 0
  | some n := n
  end

-- Example usage
def my_value : option ℕ := some 42
def res := convert_to_nat my_value

def my_list: list ℕ := [4,3,2,1]
def val:= my_list.maximum
def maxv:= convert_to_nat val
def maxind:= my_list.index_of maxv
def list2:= my_list.remove_nth maxind
#reduce list2```

[Eric Wieser]

However, when I use the inbuilt function list.maximum, I get 'some \N' and not just a natural number. What is the intuition behind that?

What should [].maximum be, and why? nevermind, this argument only works for .minimum.