[CSMastermind]

I've been meaning to learn Lean and fascinated with the concept but syntax like:

    let rec helperMemo : Nat → HashMap Nat Nat → Nat × HashMap Nat Nat

is a big turnoff to me. I find it annoying to parse mentally. I can do it but I have to concentrate or it's easy to gloss over an important detail.

[duve02]

Hey, author here. This is actually not-great style on my part. Is the following better?

   let rec helperMemo (n : Nat) (map : HashMap Nat Nat) : Nat × HashMap Nat Nat

This is how it would usually be written. I will update the post accordingly.

[westurner]

Does aliasing the types work?

  def MemoMap := HashMap Nat Nat
  def MemoResult := Nat × MemoMap

  let rec helperMemo : Nat → MemoMap → MemoResult

[tossandthrow]

Record types would likely help a lot also.

Tupples don't really indicate what I can expect from the members.

[runeblaze]

Tbh this is exactly how I felt in my algebraic geometry class. I still remember the fear I had when reading this from the blackboard

    Defn. f: X → Y is flat ⇔ O_{Y,f(x)} → O_{X,x} flat ∀ x.

Then immediately I dropped that class. Turns out I like real analysis much more

[tikhonj]

What makes it hard to parse? The lack of parentheses? The way HashMap Nat Nat is a bit verbose and not clear at a glance? Something else?