Lean 4 "expected :=" for println?

Stream: new members

[Omri Schwarz]

Hi, all. As you can see, this question is driven by day 2 of AOC. (I'm okay with being this far behind as the point is to learn Lean not collect stars).

I have this stub of a function:

  match a with
  | "A" => 1
  | "B" => 2
  | "C" => 3
  | "X" => 1
  | "Y" => 2
  | "Z" => 3
  | z => 0

def score_round (a:String) (b: String) : Int :=
  (rock_paper_scissors a) +
  match (rock_paper_scissors a - rock_paper_scissors b )%3 with
  | 0 => 3
  | 1 => 6
  | 2 => 0
  | i => 0

-- so far so good.
open String in
open IO in
def day2 : IO Unit := do
  let inputLines := getInputLines false 2
  let splitRounds := inputLines |>.map (fun x => String.split x (fun s => s == ' '))
  println splitRounds
  let scoredRounds = list.map ( score_round .[0]! .[1]! )  splitRounds

  --  let scoredRounds := splitRounds |>.map score_round
  --println splitRounds
  --println splitRounds[0]!

#eval day2

``` The last function fails as follows:


35:0:
expected ':='
35:0:
cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors

35:0:
expected ':='
35:0:
cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors

It also adds the error "expected :=" for any line where I insert println.
I'm missing the proper syntax for taking an array/list of [ [ a,b], [c,d] ...]
and mapping it so that each pair is sent to the score_round function. But expecting := for a println?

[Chris Bailey]

let scoredRounds = list.map should be let scoredRounds := list.map

[Omri Schwarz]

indeed. Thank you. That was aembarassing