3cc603c · Idris-dev · git.iko.soy

libs/prelude/Decidable/Equality.idr+10−1

compare with master

unifiedsplit

@@ -153,7 +153,7 @@ instance DecEq a => DecEq (List a) where

153 decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil)

154 decEq (x :: xs) (y :: ys) with (decEq x y)

155 decEq (x :: xs) (x :: ys) | Yes refl with (decEq xs ys)

156− decEq (x :: xs) (x :: xs) | (Yes refl) | (Yes refl) = Yes refl -- maybe another yes refl

156+ decEq (x :: xs) (x :: xs) | (Yes refl) | (Yes refl) = Yes refl

157 decEq (x :: xs) (x :: ys) | (Yes refl) | (No p) = No (\eq => lemma_x_eq_xs_neq refl p eq)

158 decEq (x :: xs) (y :: ys) | No p with (decEq xs ys)

159 decEq (x :: xs) (y :: xs) | (No p) | (Yes refl) = No (\eq => lemma_x_neq_xs_eq p refl eq)

@@ -215,3 +215,12 @@ instance DecEq Float where

215 decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)

216 else No (really_believe_me _|_)

217

218+--------------------------------------------------------------------------------

219+-- String

220+--------------------------------------------------------------------------------

221+

222+instance DecEq String where

223+ decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)

224+ else No (really_believe_me _|_)

225+

226+

test/test038/expectednew file+29

@@ -0,0 +1,29 @@

1+True

2+False

3+True

4+False

5+True

6+False

7+True

8+False

9+True

10+False

11+False

12+True

13+False

14+True

15+True

16+False

17+True

18+False

19+True

20+False

21+False

22+True

23+False

24+False

25+False

26+True

27+False

28+True

29+False

test/test038/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ -o test038 test038.idr --nocolour

3+./test038

4+rm -f test038 *.ibc

test/test038/test038.idrnew file+62

@@ -0,0 +1,62 @@

1+module Main

2+

3+test : DecEq a => a -> a -> Bool

4+test i1 i2 with (decEq i1 i2)

5+ test i1 i1 | Yes refl = True

6+ test i1 i2 | No p = False

7+

8+main : IO ()

9+main = do

10+-- Primitives

11+ putStrLn . show $ test (the Int 3) (the Int 3)

12+ putStrLn . show $ test (the Integer 3) (the Integer 4)

13+ putStrLn . show $ test "hello" "hello"

14+ putStrLn . show $ test "hello" "world"

15+ putStrLn . show $ test (the Char '\0') (the Char '\0')

16+ putStrLn . show $ test (the Char '\1') (the Char '\2')

17+-- Non-primitives

18+ -- Vect

19+ putStrLn . show $

20+ test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,3])

21+ putStrLn . show $

22+ test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,4])

23+ -- List

24+ putStrLn . show $

25+ test (the (List Int) [1,2,3]) (the (List Int) [1,2,3])

26+ putStrLn . show $

27+ test (the (List Int) [1,2,3]) (the (List Int) [1,2])

28+ putStrLn . show $

29+ test (the (List Int) [1,2,3]) (the (List Int) [1,2,4])

30+ -- Tuple

31+ putStrLn . show $

32+ test (the (Int, Int) (1, 1)) (the (Int, Int) (1, 1))

33+ putStrLn . show $

34+ test (the (Int, Int) (1, 2)) (the (Int, Int) (1, 1))

35+ -- Unit

36+ putStrLn . show $ test () ()

37+ -- Booleans

38+ putStrLn . show $ test True True

39+ putStrLn . show $ test True False

40+ -- Float

41+ putStrLn . show $ test 1.0 1.0

42+ putStrLn . show $ test 1.0 2.0

43+ -- Maybe

44+ putStrLn . show $ test (Just "hello") (Just "hello")

45+ putStrLn . show $ test (Just "hello") (Just "world")

46+ putStrLn . show $ test (Just "hello") Nothing

47+ -- Either

48+ putStrLn . show $ test (the (Either String Bool) (Left "hello"))

49+ (the (Either String Bool) (Left "hello"))

50+ putStrLn . show $ test (the (Either String Bool) (Left "hello"))

51+ (the (Either String Bool) (Left "world"))

52+ putStrLn . show $ test (Left "hello") (Right "world")

53+ putStrLn . show $ test (Left "hello") (Right False)

54+ -- Fin

55+ putStrLn . show $ test (the (Fin (S (S (S (Z))))) (fS (fS (fZ))))

56+ (the (Fin (S (S (S (Z))))) (fS (fS (fZ))))

57+ putStrLn . show $ test (the (Fin (S (S (S (Z))))) (fS (fS (fZ))))

58+ (the (Fin (S (S (S (Z))))) (fS (fZ)))

59+ -- Nat

60+ putStrLn . show $ test (S (S (S Z))) (S (S (S Z)))

61+ putStrLn . show $ test (S (S (S Z))) (S (S Z))

62+