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