git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/test/interfaces005/interfaces005.idr
53 lines 1.2 kB history raw
1module Set
2
3public export
4interface SetSig a where
5 data SetT : Type -> Type
7 new : SetT a
8 insert : a -> SetT a -> SetT a
9 member : a -> SetT a -> Bool
11Set : (a : Type) -> SetSig a => Type
12Set (a) @{sig} = SetT @{sig} a
14data Tree a = Leaf | Node (Tree a) a (Tree a)
16mkTree : Type -> Type
17mkTree = Tree
19namespace TreeSet
20 export
21 [TreeSet] Ord a => SetSig a where
23 SetT = Tree
25 new = Leaf
27 insert x Leaf = Node Leaf x Leaf
28 insert x (Node l val r) = case compare x val of
29 LT => Node (insert x l) val r
30 EQ => Node l val r
31 GT => Node l val (insert x r)
33 member x Leaf = False
34 member x (Node l val r) = case compare x val of
35 LT => member x l
36 EQ => True
37 GT => member x r
39using implementation TreeSet
41 test : Set Nat
42 test = -- insert (the Nat 3) $
43-- insert 2 $
44-- insert 7 $
45-- insert 3 $
46-- insert 4 $
47 insert {a = Nat} (the Nat 5) new
49 foo : Bool
50 foo = member (the Nat 6) test
52 bar : Bool
53 bar = member (the Nat 3) test