Mercurial > hg > Members > ryokka > HoareLogic

changeset 58:7523d5cd670b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author ryokka
date Sat, 21 Dec 2019 16:49:07 +0900
parents 990d1d892398
children 5c2cdcee9971
files whileTestGears.agda
diffstat 1 files changed, 1 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Sat Dec 21 16:35:54 2019 +0900
+++ b/whileTestGears.agda	Sat Dec 21 16:49:07 2019 +0900
@@ -185,5 +185,4 @@
 
 {-# TERMINATING #-}
 Proof : (c :  ℕ ) → whileTestPCallwP c
-Proof zero = whileTestPwP {_} {_} zero (λ env s → refl)
-Proof (suc c) = Proof (suc c)
+Proof c = Proof c