repos / jolie.agda.git

commit

417008d

parent

485cdaf

author

Eugene Akentyev

date

2016-11-05 02:12:25 +0400 +04

TypeTree yes case

 1@@ -2,8 +2,10 @@ module Type where
 2 
 3 open import Relation.Nullary
 4 open import Relation.Binary
 5-open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl)
 6+open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; cong; cong₂)
 7+open import Function using (_∘_)
 8 open import Data.Nat using (ℕ)
 9+open import Data.Empty
10 open import Data.String using (String)
11 open import Data.List using (List)
12 open import Data.Vec using (Vec)
13@@ -87,11 +89,15 @@ data TypeTree where
14   leaf : BasicType → TypeTree
15   node : BasicType → List ChildType → TypeTree
16 
17+get-basic : TypeTree → BasicType
18+get-basic (leaf b) = b
19+get-basic (node b _) = b
20+
21 module TypeTreeEq where
22   _≟_ : Decidable {A = TypeTree} _≡_
23   (leaf b1) ≟ (leaf b2) with BasicTypeEq._≟_ b1 b2
24-  ... | yes b1≡b2 = {!!}
25-  ... | no ¬b1≡b2 = no {!!}
26+  ... | yes b1≡b2 = yes (cong leaf b1≡b2)
27+  ... | no b1≢b2 = no {!!} -- ¬ leaf b1 ≡ leaf b2
28   (node b1 cts) ≟ (node b2 cts') = {!!}
29   (leaf _) ≟ (node _ _) = no λ ()
30   (node _ _) ≟ (leaf _) = no λ ()