5 ms·
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 b
by CSMastermind 1y ago
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.
- deleted 1y ago[deleted]
- duve02 1y agoHey, 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.
- runeblaze 1y agoTbh 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
- westurner 1y agoDoes aliasing the types work? def MemoMap := HashMap Nat Nat def MemoResult := Nat × MemoMap let rec helperMemo : Nat → MemoMap → MemoResult
- tossandthrow 1y agoRecord types would likely help a lot also. Tupples don't really indicate what I can expect from the members.
- tikhonj 1y agoWhat 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?