Mercurial > hg > Papers > 2019 > oshiro-thesis

annotate final_main/src/AgdaDebug.agda @ 0:83f997abf3b5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
first commit
author e155702
date Thu, 14 Feb 2019 16:51:50 +0900
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
83f997abf3b5 first commit
e155702
parents:
diff changeset
1 open import Level renaming (suc to succ ; zero to Zero )
83f997abf3b5 first commit
e155702
parents:
diff changeset
2
83f997abf3b5 first commit
e155702
parents:
diff changeset
3 module AgdaDebug where
83f997abf3b5 first commit
e155702
parents:
diff changeset
4
83f997abf3b5 first commit
e155702
parents:
diff changeset
5 open import stack
83f997abf3b5 first commit
e155702
parents:
diff changeset
6
83f997abf3b5 first commit
e155702
parents:
diff changeset
7 open import Relation.Binary.PropositionalEquality
83f997abf3b5 first commit
e155702
parents:
diff changeset
8 open import Relation.Binary.Core
83f997abf3b5 first commit
e155702
parents:
diff changeset
9 open import Data.Nat
83f997abf3b5 first commit
e155702
parents:
diff changeset
10 open import Function
83f997abf3b5 first commit
e155702
parents:
diff changeset
11
83f997abf3b5 first commit
e155702
parents:
diff changeset
12
83f997abf3b5 first commit
e155702
parents:
diff changeset
13 open SingleLinkedStack
83f997abf3b5 first commit
e155702
parents:
diff changeset
14 open Stack
83f997abf3b5 first commit
e155702
parents:
diff changeset
15
83f997abf3b5 first commit
e155702
parents:
diff changeset
16 testStack07 : {m : Level } -> Maybe (Element ℕ)
83f997abf3b5 first commit
e155702
parents:
diff changeset
17 testStack07 = pushSingleLinkedStack emptySingleLinkedStack 1 (\s -> pushSingleLinkedStack s 2 (\s -> top s))
83f997abf3b5 first commit
e155702
parents:
diff changeset
18
83f997abf3b5 first commit
e155702
parents:
diff changeset
19 testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1
83f997abf3b5 first commit
e155702
parents:
diff changeset
20 $ \s -> pushSingleLinkedStack s 2
83f997abf3b5 first commit
e155702
parents:
diff changeset
21 $ \s -> pushSingleLinkedStack s 3
83f997abf3b5 first commit
e155702
parents:
diff changeset
22 $ \s -> pushSingleLinkedStack s 4
83f997abf3b5 first commit
e155702
parents:
diff changeset
23 $ \s -> pushSingleLinkedStack s 5
83f997abf3b5 first commit
e155702
parents:
diff changeset
24 $ \s -> top s
83f997abf3b5 first commit
e155702
parents:
diff changeset
25
83f997abf3b5 first commit
e155702
parents:
diff changeset
26
83f997abf3b5 first commit
e155702
parents:
diff changeset
27 testStack10 = pushStack emptySingleLinkedStack 1
83f997abf3b5 first commit
e155702
parents:
diff changeset
28 $ \s -> pushStack 2
83f997abf3b5 first commit
e155702
parents:
diff changeset
29 $ \s -> pushStack 3
83f997abf3b5 first commit
e155702
parents:
diff changeset
30 $ \s -> pushStack 4
83f997abf3b5 first commit
e155702
parents:
diff changeset
31 $ \s -> pushStack 5
83f997abf3b5 first commit
e155702
parents:
diff changeset
32 $ \s -> top s