fb233c9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Eq class, Nat is a Num

fb233c9Edwin Brady15 years ago

lib/builtins.idr+21−6

compare with master

unifiedsplit

@@ -56,6 +56,10 @@ infix 4 &&, ||;

56(&&) True x = x;

57(&&) False _ = False;

59+not : Bool -> Bool;

60+not True = False;

61+not False = True;

62+

59infixl 5 ==, /=, ==.;

63infixl 5 ==, /=, ==.;

60infixl 6 <, <=, >, >=, <., <=., >., >=.;

64infixl 6 <, <=, >, >=, <., <=., >., >=.;

61infixl 7 <<, >>;

65infixl 7 <<, >>;

@@ -92,12 +96,26 @@ instance numInt = NumInstance prim__addInt prim__subInt prim__mulInt;

92instance numFloat : Num Float;

96instance numFloat : Num Float;

93instance numFloat = NumInstance prim__addFloat prim__subFloat prim__mulFloat;

97instance numFloat = NumInstance prim__addFloat prim__subFloat prim__mulFloat;

99+data Eq : Set -> Set where

100+ EqInstance : (eq : a -> a -> Bool) ->

101+ (neq : a -> a -> Bool) ->

102+ Eq a;

103+

104+ (==) : Eq a => a -> a -> Bool;

105+ (==) {{EqInstance eq neq}} x y = eq x y;

106+

107+ (/=) : Eq a => a -> a -> Bool;

108+ (/=) {{EqInstance eq neq}} x y = neq x y;

109+

110+instance EqInt : Eq Int;

111+instance EqInt = EqInstance (boolOp prim__eqInt) (\x, y => not (x == y));

112+

113+instance EqFloat : Eq Float;

114+instance EqFloat = EqInstance (boolOp prim__eqFloat)(\x, y => not (x == y));

115+

95div : Int -> Int -> Int;

116div : Int -> Int -> Int;

96div = prim__divInt;

117div = prim__divInt;

118

98−(==) : Int -> Int -> Bool;

99−(==) = boolOp prim__eqInt;

100−

101(<) : Int -> Int -> Bool;

119(<) : Int -> Int -> Bool;

102(<) = boolOp prim__ltInt;

120(<) = boolOp prim__ltInt;

103

121

@@ -113,9 +131,6 @@ div = prim__divInt;

113(/) : Float -> Float -> Float;

131(/) : Float -> Float -> Float;

114(/) = prim__divFloat;

132(/) = prim__divFloat;

115

133

116−(==.) : Float -> Float -> Bool;

117−(==.) = boolOp prim__eqFloat;

118−

119(<.) : Float -> Float -> Bool;

134(<.) : Float -> Float -> Bool;

120(<.) = boolOp prim__ltFloat;

135(<.) = boolOp prim__ltFloat;

121

136

lib/maybe.idr+4

@@ -5,3 +5,7 @@ maybe : b -> (a -> b) -> Maybe a -> b;

5maybe n j Nothing = n;

6maybe n j (Just x) = j x;

8+maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b;

9+maybe_bind Nothing k = Nothing;

10+maybe_bind (Just x) k = k x;

11+

lib/nat.idr+15−14

@@ -9,15 +9,27 @@ plus (S k) y = S (plus k y);

9eqRespS : m = n -> S m = S n;

10eqRespS refl = refl;

12+sub : Nat -> Nat -> Nat;

13+sub O y = O;

14+sub (S k) (S y) = sub k y;

15+sub x O = x;

16+

17+mult : Nat -> Nat -> Nat;

18+mult O y = O;

19+mult (S k) y = plus y (mult k y);

20+

21+instance numNat : Num Nat;

22+instance numNat = NumInstance plus sub mult;

23+

12−plusnO : (m : Nat) -> plus m O = m;

24+plusnO : (m : Nat) -> m + O = m;

13plusnO O = refl;

25plusnO O = refl;

14plusnO (S k) = eqRespS (plusnO k);

26plusnO (S k) = eqRespS (plusnO k);

16−plusn_Sm : (n : Nat) -> (m : Nat) -> plus n (S m) = S (plus n m);

28+plusn_Sm : (n : Nat) -> (m : Nat) -> n + S m = S (n + m);

17plusn_Sm O m = refl;

29plusn_Sm O m = refl;

18plusn_Sm (S j) m = eqRespS (plusn_Sm _ _);

30plusn_Sm (S j) m = eqRespS (plusn_Sm _ _);

20−plus_commutes : (n : Nat) -> (m : Nat) -> plus n m = plus m n;

32+plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n;

21plus_commutes O m = sym (plusnO m);

33plus_commutes O m = sym (plusnO m);

22plus_commutes (S k) m = let ih = plus_commutes k m in ?plus_commutes_Sk;

34plus_commutes (S k) m = let ih = plus_commutes k m in ?plus_commutes_Sk;

@@ -28,14 +40,3 @@ plus_commutes_Sk = proof {

28 refine plusn_Sm;

40 refine plusn_Sm;

29};

41};

31−sub : Nat -> Nat -> Nat;

32−sub O y = O;

33−sub (S k) (S y) = sub k y;

34−sub x O = x;

35−

36−mult : Nat -> Nat -> Nat;

37−mult O y = O;

38−mult (S k) y = plus y (mult k y);

39−

40−instance numNat : Num Nat;

41−instance numNat = NumInstance plus sub mult;