Mercurial > hg > Gears > GearsAgda

diff RedBlackTree.agda @ 545:b180dc78abcf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add someTest
author ryokka
date Fri, 12 Jan 2018 18:30:05 +0900
parents 1595dd84fc3e
children bc3208d510cd
line wrap: on
line diff
--- a/RedBlackTree.agda	Thu Jan 11 18:54:56 2018 +0900
+++ b/RedBlackTree.agda	Fri Jan 12 18:30:05 2018 +0900
@@ -209,15 +209,17 @@
 
 open import Data.Nat hiding (compare)
 
+compareℕ :  ℕ → ℕ → CompareResult {Level.zero}
+compareℕ x y with Data.Nat.compare x y
+... | less _ _ = LT
+... | equal _ = EQ
+... | greater _ _ = GT
+
+
 createEmptyRedBlackTreeℕ : { m : Level } (a : Set Level.zero) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ 
 createEmptyRedBlackTreeℕ  {m} a {t} = record {
         root = Nothing
      ;  nodeStack = emptySingleLinkedStack
-     ;  compare = compare1
-   } where
-       compare1 :  ℕ → ℕ → CompareResult {Level.zero}
-       compare1 x y with Data.Nat.compare x y
-       ... | less _ _ = LT
-       ... | equal _ = EQ
-       ... | greater _ _ = GT
-
+     ;  compare = compareℕ
+   }
+