view final_pre/src/AgdaStackSomeState.agda @ 11:ef87093f92d4

add pdf
author e155702
date Sun, 17 Feb 2019 17:13:37 +0900
parents 0e8b9646d43f
children
line wrap: on
line source

stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t}  ( SingleLinkedStack  D )
stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }