Comment on Verified dynamic programming with Σ-types in LeanparentComments−almostgotcaught1ya distinction without a difference wrt what i'm pointing out: this proof uses exactly zero mathematics just effectively checks all the values of maxDollars_spec.
Comments
a distinction without a difference wrt what i'm pointing out: this proof uses exactly zero mathematics just effectively checks all the values of maxDollars_spec.