Mercurial > hg > Papers > 2020 > soto-midterm

comparison src/AgdaDebug.agda @ 1:73127e0ab57c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
(none)
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 08 Sep 2020 18:38:08 +0900
parents
children
comparison
equal deleted inserted replaced
0:b919985837a3 1:73127e0ab57c
1 open import Level renaming (suc to succ ; zero to Zero )
2
3 module AgdaDebug where
4
5 open import stack
6
7 open import Relation.Binary.PropositionalEquality
8 open import Relation.Binary.Core
9 open import Data.Nat
10 open import Function
11
12
13 open SingleLinkedStack
14 open Stack
15
16 testStack07 : {m : Level } -> Maybe (Element ℕ)
17 testStack07 = pushSingleLinkedStack emptySingleLinkedStack 1 (\s -> pushSingleLinkedStack s 2 (\s -> top s))
18
19 testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1
20 $ \s -> pushSingleLinkedStack s 2
21 $ \s -> pushSingleLinkedStack s 3
22 $ \s -> pushSingleLinkedStack s 4
23 $ \s -> pushSingleLinkedStack s 5
24 $ \s -> top s
25
26
27 testStack10 = pushStack emptySingleLinkedStack 1
28 $ \s -> pushStack 2
29 $ \s -> pushStack 3
30 $ \s -> pushStack 4
31 $ \s -> pushStack 5
32 $ \s -> top s