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} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ 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} @$\rightarrow$@ 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} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a)
createSingleLinkedStack = record {
                            stack = emptySingleLinkedStack ;
                            stackMethods = singleLinkedStackSpec
                          }