Mercurial > hg > Papers > 2020 > ryokka-master
diff paper/src/cbc-condition.agda.replaced @ 9:95a5f8e76944
fix cbc_agda, cbc_hoare and Conclusion.tex
| author | ryokka |
|---|---|
| date | Fri, 07 Feb 2020 21:40:26 +0900 |
| parents | |
| children | e8655e0264b8 |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/cbc-condition.agda.replaced Fri Feb 07 21:40:26 2020 +0900 @@ -0,0 +1,9 @@ +data whileTestState : Set where + s1 : whileTestState + s2 : whileTestState + sf : whileTestState + +whileTestStateP : whileTestState @$\rightarrow$@ Envc @$\rightarrow$@ Set +whileTestStateP s1 env = (vari env @$\equiv$@ 0) /\ (varn env @$\equiv$@ c10 env) +whileTestStateP s2 env = (varn env + vari env @$\equiv$@ c10 env) +whileTestStateP sf env = (vari env @$\equiv$@ c10 env)