Mercurial > hg > Papers > 2020 > soto-midterm
diff src/AgdaDebug.agda.replaced @ 1:73127e0ab57c
(none)
author | soto@cr.ie.u-ryukyu.ac.jp |
---|---|
date | Tue, 08 Sep 2020 18:38:08 +0900 |
parents | |
children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/AgdaDebug.agda.replaced Tue Sep 08 18:38:08 2020 +0900 @@ -0,0 +1,32 @@ +open import Level renaming (suc to succ ; zero to Zero ) + +module AgdaDebug where + +open import stack + +open import Relation.Binary.PropositionalEquality +open import Relation.Binary.Core +open import Data.Nat +open import Function + + +open SingleLinkedStack +open Stack + +testStack07 : {m : Level } @$\rightarrow$@ Maybe (Element @$\mathbb{N}$@) +testStack07 = pushSingleLinkedStack emptySingleLinkedStack 1 (\s @$\rightarrow$@ pushSingleLinkedStack s 2 (\s @$\rightarrow$@ top s)) + +testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1 + $ \s @$\rightarrow$@ pushSingleLinkedStack s 2 + $ \s @$\rightarrow$@ pushSingleLinkedStack s 3 + $ \s @$\rightarrow$@ pushSingleLinkedStack s 4 + $ \s @$\rightarrow$@ pushSingleLinkedStack s 5 + $ \s @$\rightarrow$@ top s + + +testStack10 = pushStack emptySingleLinkedStack 1 + $ \s @$\rightarrow$@ pushStack 2 + $ \s @$\rightarrow$@ pushStack 3 + $ \s @$\rightarrow$@ pushStack 4 + $ \s @$\rightarrow$@ pushStack 5 + $ \s @$\rightarrow$@ top s