Comment on Verified dynamic programming with Σ-types in LeanparentComments−duve021yHey, 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.
Comments
Hey, author here. This is actually not-great style on my part. Is the following better?
This is how it would usually be written. I will update the post accordingly.