Mercurial > hg > Papers > 2020 > soto-midterm
annotate src/cbc-hoare.agda.replaced @ 1:73127e0ab57c
(none)
| author | soto@cr.ie.u-ryukyu.ac.jp |
|---|---|
| date | Tue, 08 Sep 2020 18:38:08 +0900 |
| parents | |
| children |
| rev | line source |
|---|---|
| 1 | 1 whileTestPwP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ ((env : Envc ) @$\rightarrow$@ whileTestStateP s1 env @$\rightarrow$@ t) @$\rightarrow$@ t |
| 2 whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where | |
| 3 env : Envc | |
| 4 env = whileTestP c10 ( @$\lambda$@ env @$\rightarrow$@ env ) | |
| 5 | |
| 6 loopPwP' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ whileTestStateP s2 env @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ whileTestStateP sf env @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 7 loopPwP' zero env refl refl exit = exit env refl | |
| 8 loopPwP' (suc n) env refl refl exit = whileLoopPwP' (suc n) env refl refl (@$\lambda$@ env x y @$\rightarrow$@ loopPwP' n env x y exit) exit | |
| 9 | |
| 10 | |
| 11 whileTestPCallwP' : (c : @$\mathbb{N}$@ ) @$\rightarrow$@ Set | |
| 12 whileTestPCallwP' c = whileTestPwP {_} {_} c (@$\lambda$@ env s @$\rightarrow$@ loopPwP' (varn env) env refl (conv env s) ( @$\lambda$@ env s @$\rightarrow$@ vari env @$\equiv$@ c10 env ) ) | |
| 13 | |
| 14 |