Comment on Verified dynamic programming with Σ-types in LeanparentComments−almostgotcaught1yi don't know what you're saying - here is the proof that is described in the article:1. build a table tab[n]2. check that for every i, tab[i] == maxDollars_spec[i]if you take the latter approach i proposed (bottom up) there is nothing to check the totality of.
Comments
i don't know what you're saying - here is the proof that is described in the article:
1. build a table tab[n]
2. check that for every i, tab[i] == maxDollars_spec[i]
if you take the latter approach i proposed (bottom up) there is nothing to check the totality of.