Mercurial > hg > Papers > 2018 > ryokka-sigos

comparison Paper/src/AgdaStackImpl.agda @ 3:576637483425

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix section, source code,etc
author ryokka
date Thu, 19 Apr 2018 20:28:12 +0900
parents bf2887cd22c1
children 35d15c091cfd
comparison
equal deleted inserted replaced
2:43e263faf88b 3:576637483425
13 13
14 singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a) 14 singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
15 singleLinkedStackSpec = record { 15 singleLinkedStackSpec = record {
16 push = pushSingleLinkedStack 16 push = pushSingleLinkedStack
17 ; pop = popSingleLinkedStack 17 ; pop = popSingleLinkedStack
18 ; pop2 = pop2SingleLinkedStack
19 ; get = getSingleLinkedStack 18 ; get = getSingleLinkedStack
20 ; get2 = get2SingleLinkedStack
21 ; clear = clearSingleLinkedStack
22 } 19 }
23 20
24 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a) 21 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
25 createSingleLinkedStack = record { 22 createSingleLinkedStack = record {
26 stack = emptySingleLinkedStack ; 23 stack = emptySingleLinkedStack ;