local type alias

Stream: general

[Alexandre Rademaker]

Can I make the declaration of tf local to collapse₃?

def tf := List Int → List Int

def collapse₃ (xss : List (List Int)) : List Int :=
  help (0, id) (labelsum xss) []
  where
    sum (xs : List Int) := xs.foldl Int.add 0
    labelsum (xss : List (List Int)) : List (Int × List Int) :=
     List.zip (map sum xss) xss
    help : (Int × tf) → List (Int × List Int) → tf
    | (_, f), [] => f
    | (s, f), (as :: bs) =>
      if s > 0 then f
      else help (s + as.1, f ∘ (as.2 ++ ·)) bs

[Johan Commelin]

open List

def collapse₃ (xss : List (List Int)) : List Int :=
  help (0, id) (labelsum xss) []
  where
    sum (xs : List Int) := xs.foldl Int.add 0
    labelsum (xss : List (List Int)) : List (Int × List Int) :=
     List.zip (map sum xss) xss
    help :
      let tf := List Int → List Int -- <--------- voila
      (Int × tf) → List (Int × List Int) → tf
    | (_, f), [] => f
    | (s, f), (as :: bs) =>
      if s > 0 then f
      else help (s + as.1, f ∘ (as.2 ++ ·))

[Alexandre Rademaker]

oh great!! I don't know why the let in the collapse₃ beginning didn't work.. Anyway, nice to know where to put a let when using the Pattern-Matching Definitions.