Skip to content

Comment on Verified dynamic programming with Σ-types in Leanparent

Comments

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.
AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.