From 417008d23c8aabf22cb044051993f0f07061c6c2 Mon Sep 17 00:00:00 2001
From: Eugene Akentyev <ak3ntev@gmail.com>
Date: Sat, 5 Nov 2016 01:12:25 +0300
Subject: [PATCH] TypeTree yes case

---
 src/Type.agda | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/Type.agda b/src/Type.agda
index 48a00af..0d0da46 100644
--- a/src/Type.agda
+++ b/src/Type.agda
@@ -2,8 +2,10 @@ module Type where
 
 open import Relation.Nullary
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; cong; cong₂)
+open import Function using (_∘_)
 open import Data.Nat using (ℕ)
+open import Data.Empty
 open import Data.String using (String)
 open import Data.List using (List)
 open import Data.Vec using (Vec)
@@ -87,11 +89,15 @@ data TypeTree where
   leaf : BasicType → TypeTree
   node : BasicType → List ChildType → TypeTree
 
+get-basic : TypeTree → BasicType
+get-basic (leaf b) = b
+get-basic (node b _) = b
+
 module TypeTreeEq where
   _≟_ : Decidable {A = TypeTree} _≡_
   (leaf b1) ≟ (leaf b2) with BasicTypeEq._≟_ b1 b2
-  ... | yes b1≡b2 = {!!}
-  ... | no ¬b1≡b2 = no {!!}
+  ... | yes b1≡b2 = yes (cong leaf b1≡b2)
+  ... | no b1≢b2 = no {!!} -- ¬ leaf b1 ≡ leaf b2
   (node b1 cts) ≟ (node b2 cts') = {!!}
   (leaf _) ≟ (node _ _) = no λ ()
   (node _ _) ≟ (leaf _) = no λ ()
-- 
2.50.1