Mercurial > hg > Papers > 2023 > soto-master
diff Paper/src/while_loop_verif/init_cg.agda @ 1:a72446879486
Init paper
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 12 Jan 2023 20:28:50 +0900 |
| parents | |
| children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_verif/init_cg.agda Thu Jan 12 20:28:50 2023 +0900 @@ -0,0 +1,7 @@ +whileTest' : {l : Level} {t : Set l} → {c10 : ℕ } → (Code : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t +whileTest' {_} {_} {c10} next = next env proof2 + where + env : Env + env = record {vari = 0 ; varn = c10} + proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition + proof2 = record {pi1 = refl ; pi2 = refl}