match gaurds

Stream: lean4

[Joseph O]

how do i fix this type error

def allPairsAux (xs: List α) (ys: List β) (accum: List (α × β)) :=
  match xs, ys with
  | _, [] => accum
  | [], _ => accum
  | x::xs, y::ys =>
    allPairsAux xs ys ((x, y)::accum)

type mismatch
  accum
has type
  List (α × β) : Type (max ?u.18 ?u.15)
but is expected to have type
  ?m.166 : Sort ?u.25

[Joseph O]

should i write out the return type?

[Joseph O]

yeah that fixed it

[Joseph O]

excuse my previous question, i have a new one:

how can i have gaurds on patterns, like in f# i can do

match x with

[Wojciech Nawrocki]

Afaik Lean doesn't support pattern guards, so you would just write => if x > 5 then .. else ...

[Kyle Miller]

Here's a hacky way to have a pattern guard, where you add an additional boolean discriminant:

notation:50 e:51 " matches " p:0 " where " f:0 => ((match e with | p => f | _ => false) : Bool)

def foo (l : List Nat) : List Nat :=
  match l, l matches (x :: _) where x > 5 with
  | (x :: xs), true => xs
  | _, _ => l

The matches notation gave me the idea.

[Joseph O]

Man, @Kyle Miller you are the master of hacky solutions