Mercurial > hg > Papers > 2019 > oshiro-thesis

view final_pre/src/AgdaStack.agda @ 7:0e8b9646d43f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add final_pre
author e155702
date Sun, 17 Feb 2019 05:39:59 +0900
parents
children
line wrap: on
line source

data Element (a : Set) : Set where
  cons : a -> Maybe (Element a) -> Element a

datum : {a : Set} -> Element a -> a
datum (cons a _) = a

next : {a : Set} -> Element a -> Maybe (Element a)
next (cons _ n) = n

record SingleLinkedStack (a : Set) : Set where
  field
    top : Maybe (Element a)