Mercurial > hg > Papers > 2020 > ryokka-master

comparison paper/src/AgdaDebug.agda.replaced @ 2:c7acb9211784

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add code, figure. and paper fix content
author ryokka
date Mon, 27 Jan 2020 20:41:36 +0900
parents
children
comparison
equal deleted inserted replaced
1:ee44dbda6bd3 2:c7acb9211784
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 } @$\rightarrow$@ Maybe (Element @$\mathbb{N}$@)
17 testStack07 = pushSingleLinkedStack emptySingleLinkedStack 1 (\s @$\rightarrow$@ pushSingleLinkedStack s 2 (\s @$\rightarrow$@ top s))
18
19 testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1
20 $ \s @$\rightarrow$@ pushSingleLinkedStack s 2
21 $ \s @$\rightarrow$@ pushSingleLinkedStack s 3
22 $ \s @$\rightarrow$@ pushSingleLinkedStack s 4
23 $ \s @$\rightarrow$@ pushSingleLinkedStack s 5
24 $ \s @$\rightarrow$@ top s
25
26
27 testStack10 = pushStack emptySingleLinkedStack 1
28 $ \s @$\rightarrow$@ pushStack 2
29 $ \s @$\rightarrow$@ pushStack 3
30 $ \s @$\rightarrow$@ pushStack 4
31 $ \s @$\rightarrow$@ pushStack 5
32 $ \s @$\rightarrow$@ top s