Mercurial > hg > Gears > GearsAgda
diff stackTest.agda @ 541:429ece770187
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 11 Jan 2018 15:16:44 +0900 |
| parents | 5c001e8ba0d5 |
| children | 0b791ae19543 |
line wrap: on
line diff
--- a/stackTest.agda Thu Jan 11 11:55:22 2018 +0900 +++ b/stackTest.agda Thu Jan 11 15:16:44 2018 +0900 @@ -6,6 +6,7 @@ open import Relation.Binary.PropositionalEquality open import Relation.Binary.Core open import Data.Nat +open import Function open SingleLinkedStack @@ -69,6 +70,12 @@ testStack07 = pushSingleLinkedStack emptySingleLinkedStack 1 ( \s -> pushSingleLinkedStack s 2 (\s -> top s)) +testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1 + $ \s -> pushSingleLinkedStack s 2 + $ \s -> pushSingleLinkedStack s 3 + $ \s -> pushSingleLinkedStack s 4 + $ \s -> pushSingleLinkedStack s 5 + $ \s -> top s ------ -- @@ -89,8 +96,8 @@ push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl } -id : {n : Level} {A : Set n} -> A -> A -id a = a +-- id : {n : Level} {A : Set n} -> A -> A +-- id a = a -- push a, n times