Mercurial > hg > Papers > 2021 > soto-prosym
comparison Paper/src/cbc-condition.agda.replaced @ 0:c59202657321
init
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 02 Nov 2021 06:55:58 +0900 |
| parents | |
| children | 339fb67b4375 |
comparison
equal
deleted
inserted
replaced
| -1:000000000000 | 0:c59202657321 |
|---|---|
| 1 data whileTestState : Set where | |
| 2 s1 : whileTestState | |
| 3 s2 : whileTestState | |
| 4 sf : whileTestState | |
| 5 | |
| 6 whileTestStateP : whileTestState @$\rightarrow$@ Envc @$\rightarrow$@ Set | |
| 7 whileTestStateP s1 env = (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) | |
| 8 whileTestStateP s2 env = (varn env + vari env @$\equiv$@ c10 env) | |
| 9 whileTestStateP sf env = (vari env @$\equiv$@ c10 env) |