Nice job. My attempt at the initial strong induction proof was a long time ago so I don't remember the details. It definitely followed a similar structure as yours (but this was before `omega` im pretty sure). Can't…
Great breakdown of this. Thanks.
> You could write this same proof in absolutely any language that supports recursion Well, you at least need dependent types just to state the theorem, which eliminates nearly all other languages.
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…
Nice job. My attempt at the initial strong induction proof was a long time ago so I don't remember the details. It definitely followed a similar structure as yours (but this was before `omega` im pretty sure). Can't…
Great breakdown of this. Thanks.
> You could write this same proof in absolutely any language that supports recursion Well, you at least need dependent types just to state the theorem, which eliminates nearly all other languages.
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…