# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1483245362 0
# Node ID 5af5f1a930bc1d5e9e549a2e049e77eb19471dae
# Parent  dc6a09d4f90061ad9a033928003ef1ab60ad425c
Trying Set with constraint...

diff -r dc6a09d4f900 -r 5af5f1a930bc sandbox/SetWithConstraint.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/sandbox/SetWithConstraint.agda	Sun Jan 01 04:36:02 2017 +0000
@@ -0,0 +1,30 @@
+module SetWithConstraint where
+
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+open import Function
+open import Data.Bool
+open import Data.Nat
+open import Data.Nat.Properties
+open import Data.List
+open import Data.Product
+open import Data.AVL 
+open import Data.AVL.Sets (Relation.Binary.StrictTotalOrder.isStrictTotalOrder Data.Nat.Properties.strictTotalOrder) as S
+
+yo : ⟨Set⟩
+yo = S.empty
+
+empty-set : (length (S.toList  S.empty)) ≡ zero
+empty-set  = refl
+
+empty-set+1 : length (S.toList (S.insert 100 S.empty)) ≡ 1
+empty-set+1 = refl
+
+open ≡-Reasoning
+
+non-empty-set+1 : (a : ℕ ) (s : ⟨Set⟩) {notElem : (a S.∈? s) ≡ false} -> length (S.toList (S.insert a s)) ≡ suc (length (S.toList s))
+non-empty-set+1 a (tree (Indexed.leaf l<u))         = refl
+non-empty-set+1 a (tree (Indexed.node (proj₃ , proj₄) x x₁ Height-invariants.∼+)) = {!!}
+non-empty-set+1 a (tree (Indexed.node (proj₃ , proj₄) x x₁ Height-invariants.∼0)) = {!!}
+non-empty-set+1 a (tree (Indexed.node (proj₃ , proj₄) x x₁ Height-invariants.∼-)) = {!!}
+