Creating iterative loop

Stream: new members

[Vivek Rajesh Joshi]

I want to make an iterative loop that traverses over each row of a matrix (each sub-array of a 2D array). for .. do withList.range keeps giving the error of invalid 'do' notation, expected type is not a monad application -- (return type of loop). What should I do here?
Here's the loop I want to make:

def is_rrf_row (i : Fin r → Rat) : Bool :=
  let ri := List.ofFn i
  let should_0 := ri.take (List.indexOf 1 ri)
  if should_0 = List.replicate (List.indexOf 1 ri) 0 then True
  else False

def isrrfMat (M : Matrix (Fin r) (Fin s) Rat) : Prop :=
  let bl := []
  for i in (List.range r) do         --Not working
    if is_rrf_row (M i) then bl.insert 1
    else 0
  if bl.prod == 1 then True
  else False

Basically I want to check whether all rows of a matrix satisfy is_rrf_row

[Eric Wieser]

Try adding Id.run do after the first :=

[Vivek Rajesh Joshi]

It's still highlighting the return type as the problem (don't know how to synthesize implicit argument). Giving Prop as an argument highlights the let below and says expected command.
I thought the return type was the problem, so I removed it. This is where I have reached now:

def isrrfMat (M : Matrix (Fin r) (Fin s) Rat) :=
  let bl := []
  for i in (List.finRange r) do
    if is_rrf_row (M i) then bl.insert 1
    else bl.insert 0

#eval isrrfMat !![1,2,3;4,5,6;7,8,(9:Rat)]     --Result: [PUnit.unit]

[Vivek Rajesh Joshi]

Does anyone have a fix for the above code, or another way to do the loop?

[Anand Rao Tadipatri]

Here is how the code can be modified to work:

import Mathlib

def is_rrf_row (i : Fin r → Rat) : Bool :=
  let ri := List.ofFn i
  let should_0 := ri.take (List.indexOf 1 ri)
  if should_0 = List.replicate (List.indexOf 1 ri) 0 then True
  else False

def isrrfMat (M : Matrix (Fin r) (Fin s) Rat) : Prop := Id.run do -- to allow imperative syntax in Lean
  let mut bl := [] -- the list must be marked mutable
  for h:i in List.range r do -- `h` is the proof that `i ∈ List.range r`
    if is_rrf_row (M ⟨i, List.mem_range.mp h⟩) then  -- `i` needs to be converted to type `Fin r`
      bl := bl.insert 1 -- `bl` is assigned the new value
    else
      bl := bl.insert 0
  if bl.prod == 1 then True
  else False

[Vivek Rajesh Joshi]

I see, thanks!