Mercurial > hg > Members > ryokka > HoareLogic

diff whileTestPrim.agda @ 93:a7263ecf8671

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 01 Nov 2021 09:59:43 +0900
parents 07b183a726f6
children
line wrap: on
line diff
--- a/whileTestPrim.agda	Mon Nov 01 08:34:07 2021 +0900
+++ b/whileTestPrim.agda	Mon Nov 01 09:59:43 2021 +0900
@@ -1,7 +1,7 @@
 module whileTestPrim where
 
 open import Function
-open import Data.Nat
+open import Data.Nat renaming ( _∸_ to _-_)
 open import Data.Bool hiding ( _≟_ )
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Relation.Nullary using (¬_; Dec; yes; no)