--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/stackImpl.agda	Mon Jan 27 20:41:36 2020 +0900
@@ -0,0 +1,38 @@
+record Element {l : Level} (a : Set l) : Set l where
+  inductive
+  constructor cons
+  field
+    datum : a  -- `data` is reserved by Agda.
+    next : Maybe (Element a)
+open Element
+
+record SingleLinkedStack {n : Level } (a : Set n) : Set n where
+  field
+  top : Maybe (Element a)
+open SingleLinkedStack
+
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
+pushSingleLinkedStack stack datum next = next stack1
+  where
+    element = cons datum (top stack)
+    stack1  = record {top = Just element}
+
+-- push 以下は省略
+
+-- Basic stack implementations are specifications of a Stack
+
+singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+                                   push = pushSingleLinkedStack
+                                 ; pop  = popSingleLinkedStack
+                                 ; pop2 = pop2SingleLinkedStack
+                                 ; get  = getSingleLinkedStack
+                                 ; get2 = get2SingleLinkedStack
+                                 ; clear = clearSingleLinkedStack
+                               }
+
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+                            stack = emptySingleLinkedStack ;
+                            stackMethods = singleLinkedStackSpec
+                          }