Mercurial > hg > Papers > 2020 > ryokka-master
comparison paper/src/agda-mdg.agda.replaced @ 13:e8655e0264b8
fix paper, slide
author | ryokka |
---|---|
date | Tue, 11 Feb 2020 02:31:26 +0900 |
parents | 95a5f8e76944 |
children |
comparison
equal
deleted
inserted
replaced
12:bf3288c36d7e | 13:e8655e0264b8 |
---|---|
3 s2 : whileTestState | 3 s2 : whileTestState |
4 sf : whileTestState | 4 sf : whileTestState |
5 | 5 |
6 | 6 |
7 whileTestStateP : whileTestState @$\rightarrow$@ Envc @$\rightarrow$@ Set | 7 whileTestStateP : whileTestState @$\rightarrow$@ Envc @$\rightarrow$@ Set |
8 whileTestStateP s1 env = (vari env @$\equiv$@ 0) /\ (varn env @$\equiv$@ c10 env) | 8 whileTestStateP s1 env = (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) |
9 whileTestStateP s2 env = (varn env + vari env @$\equiv$@ c10 env) | 9 whileTestStateP s2 env = (varn env + vari env @$\equiv$@ c10 env) |
10 whileTestStateP sf env = (vari env @$\equiv$@ c10 env) | 10 whileTestStateP sf env = (vari env @$\equiv$@ c10 env) |