Mercurial > hg > Papers > 2022 > soto-sigos
comparison Paper/src/AgdaStack.agda @ 0:14a0e409d574
ADD fast commit
author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 24 Apr 2022 23:13:44 +0900 |
parents | |
children |
comparison
equal
deleted
inserted
replaced
-1:000000000000 | 0:14a0e409d574 |
---|---|
1 data Element (a : Set) : Set where | |
2 cons : a -> Maybe (Element a) -> Element a | |
3 | |
4 datum : {a : Set} -> Element a -> a | |
5 datum (cons a _) = a | |
6 | |
7 next : {a : Set} -> Element a -> Maybe (Element a) | |
8 next (cons _ n) = n | |
9 | |
10 record SingleLinkedStack (a : Set) : Set where | |
11 field | |
12 top : Maybe (Element a) | |
13 |