Mercurial > hg > Papers > 2018 > ryokka-sigos
view Paper/src/AgdaTreeImpl.agda.replaced @ 6:4312a27022d1
fix
author | ryokka |
---|---|
date | Mon, 23 Apr 2018 18:11:46 +0900 |
parents | bf2887cd22c1 |
children | 06a1339fbda4 |
line wrap: on
line source
record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.$\sqcup$ n) where field putImpl : treeImpl $\rightarrow$ a $\rightarrow$ (treeImpl $\rightarrow$ t) $\rightarrow$ t getImpl : treeImpl $\rightarrow$ (treeImpl $\rightarrow$ Maybe a $\rightarrow$ t) $\rightarrow$ t record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.$\sqcup$ n) where field tree : treeImpl treeMethods : TreeMethods {n} {m} {a} {t} treeImpl putTree : a $\rightarrow$ (Tree treeImpl $\rightarrow$ t) $\rightarrow$ t putTree d next = putImpl (treeMethods ) tree d (\t1 $\rightarrow$ next (record {tree = t1 ; treeMethods = treeMethods} )) getTree : (Tree treeImpl $\rightarrow$ Maybe a $\rightarrow$ t) $\rightarrow$ t getTree next = getImpl (treeMethods ) tree (\t1 d $\rightarrow$ next (record {tree = t1 ; treeMethods = treeMethods} ) d )