git.iko.soy/Idris-dev
on d773edd help sign in
Idris-dev/test/interfaces005/interfaces005a.idr
50 lines 1.1 kB history raw
1module Set
2
3public export
4interface SetSig a where
5 data Set : Type -> Type
7 new : Set a
8 insert : a -> Set a -> Set a
9 member : a -> Set a -> Bool
11data Tree a = Leaf | Node (Tree a) a (Tree a)
13mkTree : Type -> Type
14mkTree = Tree
16namespace TreeSet
17 export
18 [TreeSet] Ord a => SetSig a where
20 Set = mkTree
22 new = Leaf
24 insert x Leaf = Node Leaf x Leaf
25 insert x (Node l val r) = case compare x val of
26 LT => Node (insert x l) val r
27 EQ => Node l val r
28 GT => Node l val (insert x r)
30 member x Leaf = False
31 member x (Node l val r) = case compare x val of
32 LT => member x l
33 EQ => True
34 GT => member x r
36using implementation TreeSet
38 test : Set @{TreeSet {a=Nat}} Nat
39 test = insert 3 $
40 insert 2 $
41 insert 7 $
42 insert 3 $
43 insert 4 $
44 insert 5 new
46 foo : Bool
47 foo = member 6 test
49 bar : Bool
50 bar = member 3 test