Mercurial > hg > Members > atton > agda > systemF

changeset 25:2efb882e120d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define Binary Tree
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 18 Apr 2014 14:03:54 +0900
parents 36d0732d28e5
children 852798763d56
files systemF.agda
diffstat 1 files changed, 19 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/systemF.agda	Wed Apr 16 16:26:25 2014 +0900
+++ b/systemF.agda	Fri Apr 18 14:03:54 2014 +0900
@@ -173,4 +173,22 @@
 --elem2-list {l} {ll} {U} {u1} {u2} = cons u1 (cons u2 nil)
 
 --lemma-list-nil-cons-val : {l ll : Level} {U : Set l} -> (ListIt {l} {U} {(l ⊔ (suc ll))} {List {l} {ll} U} (nil {l} {U} {ll}) (cons {l} {U} {ll}) elem2-list) ≡ elem2-list
---lemma-list-nil-cons-val = refl
\ No newline at end of file
+--lemma-list-nil-cons-val = refl
+
+
+-- Binary Tree
+
+data BinTree {l : Level} : Set (suc l) where
+  leaf   : BinTree
+  couple : BinTree -> BinTree -> BinTree
+
+BinTreeIt : {l : Level} -> {W : Set l} -> W -> (W -> W -> W) -> BinTree {l} -> W
+BinTreeIt w f (couple left right) = f (BinTreeIt w f left) (BinTreeIt w f right)
+BinTreeIt w f leaf = w
+
+
+lemma-binary-tree-it-leaf : {l : Level} {W : Set l} {w : W} {f : W -> W -> W} -> BinTreeIt w f leaf ≡ w
+lemma-binary-tree-it-leaf = refl
+
+lemma-binary-tree-it-tree : {l : Level} {W : Set l} {w : W} {f : W -> W -> W} {u v : BinTree} -> BinTreeIt w f (couple u v)  ≡ f (BinTreeIt w f u) (BinTreeIt w f v)
+lemma-binary-tree-it-tree = refl
\ No newline at end of file