Mercurial > hg > Members > kono > Proof > category

diff src/negnat.agda @ 1124:f683d96fbc93 default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
safe fix done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jul 2024 22:28:50 +0900
parents ac53803b3b2a
children
line wrap: on
line diff
--- a/src/negnat.agda	Sun Jul 07 17:05:16 2024 +0900
+++ b/src/negnat.agda	Sun Jul 07 22:28:50 2024 +0900
@@ -1,13 +1,14 @@
+{-# OPTIONS --cubical-compatible --safe #-}
 module negnat where
 
 
 open import Data.Nat
-open import Relation.Nullary
+open import Relation.Nullary hiding (proof)
 open import Data.Empty
 open import Data.Unit
 open import Data.Fin renaming ( suc to fsuc ; zero to fzero ; _+_ to _++_ )
 open import Relation.Binary.Core
-open import  Relation.Binary.PropositionalEquality
+open import  Relation.Binary.PropositionalEquality hiding (J)
 
 
 --  http://stackoverflow.com/questions/22580842/non-trivial-negation-in-agda