Comment on Verified dynamic programming with Σ-types in LeanparentComments−westurner1yDoes aliasing the types work? def MemoMap := HashMap Nat Nat def MemoResult := Nat × MemoMap let rec helperMemo : Nat → MemoMap → MemoResult−tossandthrow1yRecord types would likely help a lot also.Tupples don't really indicate what I can expect from the members.
Comments
Does aliasing the types work?
Record types would likely help a lot also.
Tupples don't really indicate what I can expect from the members.