changeset 5:ae72a05db7e2

add while_test_init_imple
author soto
date Thu, 11 Feb 2021 17:21:26 +0900
parents bf1f62556b81
children dcc839d6f569
files paper/src/agda/logic.agda
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/paper/src/agda/logic.agda	Thu Feb 11 17:03:31 2021 +0900
+++ b/paper/src/agda/logic.agda	Thu Feb 11 17:21:26 2021 +0900
@@ -2,7 +2,7 @@
 
 open import Level
 open import Relation.Nullary
-open import Relation.Binary
+open import Relation.Binary hiding(_⇔_)
 open import Data.Empty