Mercurial > hg > Papers > 2022 > soto-sigos
comparison Paper/src/cbc-hoare-loop.agda.replaced @ 0:14a0e409d574
ADD fast commit
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Apr 2022 23:13:44 +0900 |
| parents | |
| children |
comparison
equal
deleted
inserted
replaced
| -1:000000000000 | 0:14a0e409d574 |
|---|---|
| 1 whileLoopPwP!$\prime$! : {l : Level} {t : Set l} !$\rightarrow$! (n : !$\mathbb{N}$!) !$\rightarrow$! (env : Envc ) | |
| 2 !$\rightarrow$! (n !$\equiv$! varn env) !$\rightarrow$! whileTestStateP s2 env | |
| 3 !$\rightarrow$! (next : (env : Envc ) !$\rightarrow$! (pred n !$\equiv$! varn env) !$\rightarrow$! whileTestStateP s2 env !$\rightarrow$! t) | |
| 4 !$\rightarrow$! (exit : (env : Envc ) !$\rightarrow$! whileTestStateP sf env !$\rightarrow$! t) !$\rightarrow$! t | |
| 5 whileLoopPwP!$\prime$! zero env refl refl _ exit = exit env refl | |
| 6 whileLoopPwP!$\prime$! (suc n) env refl refl next _ = | |
| 7 next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env)) | |
| 8 | |
| 9 | |
| 10 loopPwP!$\prime$! : {l : Level} {t : Set l} !$\rightarrow$! (n : !$\mathbb{N}$!) !$\rightarrow$! (env : Envc ) | |
| 11 !$\rightarrow$! (n !$\equiv$! varn env) !$\rightarrow$! whileTestStateP s2 env | |
| 12 !$\rightarrow$! (exit : (env : Envc ) !$\rightarrow$! whileTestStateP sf env !$\rightarrow$! t) !$\rightarrow$! t | |
| 13 loopPwP!$\prime$! zero env refl refl exit = exit env refl | |
| 14 loopPwP!$\prime$! (suc n) env refl refl exit | |
| 15 = whileLoopPwP!$\prime$! (suc n) env refl refl (!$\lambda$! env x y !$\rightarrow$! loopPwP!$\prime$! n env x y exit) exit |