duve02

7 ms·

1. 1.▲
   by duve02 1y ago

   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 quite remember
2. 2.▲
   by duve02 1y ago

   Great breakdown of this. Thanks.
3. 3.▲
   by duve02 1y ago

   > 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.
4. 4.▲
   by duve02 1y ago

   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 acc