44cdd8a · Idris-dev · git.iko.soy

CHANGELOG+1

compare with master

unifiedsplit

@@ -20,6 +20,7 @@ New in 0.9.15:

20 compiler distribution only ships with the C and JavaScript backends.

21* New REPL command :printdef displays the internal definition of a name

22* New REPL command :pprint pretty-prints a definition or term with LaTeX or HTML highlighting

23+* Naming of data and type constructors is made consistent across the standard library (see #1516)

23

24

24New in 0.9.14:

25New in 0.9.14:

25--------------

26--------------

benchmarks/quasigroups/Parser.idr+8−8

@@ -24,11 +24,11 @@ parseToken x = map Just (tryParseFin ((cast x) - 1))

24 where

25 tryParseFin : Int -> Either String (Fin n)

26 tryParseFin {n=Z} _ = Left ("Given cell " ++ x ++ " out of range")

27− tryParseFin {n=S k} 0 = return fZ

27+ tryParseFin {n=S k} 0 = return FZ

28 tryParseFin {n=S k} x =

29 case tryParseFin {n=k} (x-1) of

30 Left err => Left err

31− Right fin => return (fS fin)

31+ Right fin => return (FS fin)

32

33length : Vect n a -> Nat

34length {n=n} _ = n

@@ -49,9 +49,9 @@ parseCols {n=S k} row l cs = helper last l

49 No _ => Left ("Illegal cell " ++ index x cs)

50

51 helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)

52− helper fZ l = step l fZ

52+ helper FZ l = step l FZ

53− helper (fS k) l = do

53+ helper (FS k) l = do

54− (_ ** next) <- step l (fS k)

54+ (_ ** next) <- step l (FS k)

55 helper (weaken k) next

56

57parseRows : (b : Board n) -> LegalBoard b -> Vect n String -> Parser n

@@ -66,9 +66,9 @@ parseRows {n=S k} _ l rs = helper last l

66 Yes prf => let foo = (replace {P=\n => Vect n String} prf cs) in parseCols i l foo -- TODO: foo shouldn't be needed

67

68 helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)

69− helper fZ l = step fZ l

69+ helper FZ l = step FZ l

70− helper (fS k) l = do

70+ helper (FS k) l = do

71− (_ ** next) <- step (fS k) l

71+ (_ ** next) <- step (FS k) l

72 helper (weaken k) next

73

74parse : String -> Either String (n : Nat ** (b : Board n ** LegalBoard b))

benchmarks/quasigroups/Solver.idr+14−14

@@ -35,8 +35,8 @@ instance Show (Board n) where

35 show (MkBoard rs) = unlines (map showRow rs)

36

37updateAt : Fin n -> Vect n a -> (a -> a) -> Vect n a

38−updateAt fZ (x::xs) f = f x :: xs

38+updateAt FZ (x::xs) f = f x :: xs

39−updateAt (fS i) (x::xs) f = x :: updateAt i xs f

39+updateAt (FS i) (x::xs) f = x :: updateAt i xs f

40

41setCell : Board n -> (Fin n, Fin n) -> Fin n -> Board n

42setCell (MkBoard b) (x, y) value = MkBoard (updateAt y b (\row => updateAt x row (const (Just value))))

@@ -80,7 +80,7 @@ Empty : Cell n -> Type

80Empty {n=n} x = (the (Cell n) Nothing) = x

81

82empty : (cell : Cell n) -> Dec (Empty cell)

83−empty Nothing = Yes refl

83+empty Nothing = Yes Refl

84empty (Just _) = No nothingNotJust

85

86-- Predicate for legal cell assignments

@@ -107,7 +107,7 @@ Filled {n=n} = (\x => Not (Empty x))

107--Filled {n=n} = \x => the (Maybe (Fin n)) Nothing = x -> _|_

108

109filled : (cell : Cell n) -> Dec (Filled cell)

110−filled Nothing = No (\f => f refl)

110+filled Nothing = No (\f => f Refl)

111filled (Just _) = Yes nothingNotJust

112

113FullBoard : Board n -> Type

@@ -127,18 +127,18 @@ data LegalBoard : Board n -> Type where

127CompleteBoard : Board n -> Type

128CompleteBoard b = (LegalBoard b, FullBoard b)

129

130−indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (fS i) (x::xs)

130+indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (FS i) (x::xs)

131−indexStep = refl

131+indexStep = Refl

132

133find : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a)

134 -> Either (All (\x => Not (P x)) xs) (y : a ** (P y, (i : Fin n ** y = index i xs)))

135find _ Nil = Left Nil

136find d (x::xs) with (d x)

137− | Yes prf = Right (x ** (prf, (fZ ** refl)))

137+ | Yes prf = Right (x ** (prf, (FZ ** Refl)))

138 | No prf =

139 case find d xs of

140 Right (y ** (prf', (i ** prf''))) =>

141− Right (y ** (prf', (fS i ** replace {P=(\x => y = x)} (indexStep {x=x}) prf'')))

141+ Right (y ** (prf', (FS i ** replace {P=(\x => y = x)} (indexStep {x=x}) prf'')))

142 Left prf' => Left (prf::prf')

143

144findEmptyInRow : (xs : Vect n (Cell n)) -> Either (All Filled xs) (i : Fin n ** Empty (index i xs))

@@ -158,11 +158,11 @@ emptyCell (MkBoard rs) =

158 helper Nil = Left Nil

159 helper (r::rs) =

160 case findEmptyInRow r of

161− Right (ci ** pf) => Right (fZ ** (ci ** pf))

161+ Right (ci ** pf) => Right (FZ ** (ci ** pf))

162 Left prf =>

163 case helper rs of

164 Left prf' => Left (prf::prf')

165− Right (ri ** (ci ** pf)) => Right (fS ri ** (ci ** pf))

165+ Right (ri ** (ci ** pf)) => Right (FS ri ** (ci ** pf))

166

167

168tryValue : {b : Board (S n)} -> LegalBoard b -> (c : (Fin (S n), Fin (S n))) -> Empty (getCell b c) -> (v : Fin (S n))

@@ -189,16 +189,16 @@ fillBoard {n=(S n)} b l with (emptyCell b)

189 Right success => (v, Just success)

190 Left _ => -- TODO: Prove unsolvable

191 case v of

192− fS k => tryAll (weaken k)

192+ FS k => tryAll (weaken k)

193− fZ => (v, Nothing)

193+ FZ => (v, Nothing)

194

195 %assert_total

196 recurse : Fin (S n) -> Maybe (b' : Board (S n) ** CompleteBoard b')

197 recurse start =

198 case tryAll start of

199 (_, Nothing) => Nothing

200− (fZ, Just (b' ** l')) => fillBoard b' l'

200+ (FZ, Just (b' ** l')) => fillBoard b' l'

201− (fS next, Just (b' ** l')) =>

201+ (FS next, Just (b' ** l')) =>

202 case fillBoard b' l' of

203 Just solution => Just solution

204 Nothing => recurse (weaken next)

contribs/gtksourceview-2.0-language-spec/idris.lang+1−1

@@ -216,7 +216,7 @@

216 <keyword>compute</keyword>

217 <keyword>solve</keyword>

218 <keyword>attack</keyword>

219− <keyword>refl</keyword>

219+ <keyword>Refl</keyword>

220 <keyword>state</keyword>

221 <keyword>term</keyword>

222 <keyword>undo</keyword>

libs/base/Control/Isomorphism.idr+37−37

@@ -14,9 +14,9 @@ data Iso : Type -> Type -> Type where

14

15-- Isomorphism properties

16

17−||| Isomorphism is reflexive

17+||| Isomorphism is Reflexive

18isoRefl : Iso a a

19−isoRefl = MkIso id id (\x => refl) (\x => refl)

19+isoRefl = MkIso id id (\x => Refl) (\x => Refl)

20

21||| Isomorphism is transitive

22isoTrans : Iso a b -> Iso b c -> Iso a c

@@ -43,8 +43,8 @@ eitherComm = MkIso swap swap swapSwap swapSwap

43 swap (Left x) = Right x

44 swap (Right x) = Left x

45 swapSwap : (e : Either a' b') -> swap (swap e) = e

46− swapSwap (Left x) = refl

46+ swapSwap (Left x) = Refl

47− swapSwap (Right x) = refl

47+ swapSwap (Right x) = Refl

48

49||| Disjunction is associative

50eitherAssoc : Iso (Either (Either a b) c) (Either a (Either b c))

@@ -60,14 +60,14 @@ eitherAssoc = MkIso eitherAssoc1 eitherAssoc2 ok1 ok2

60 eitherAssoc2 (Right (Right x)) = Right x

61

62 ok1 : (x : Either a (Either b c)) -> eitherAssoc1 (eitherAssoc2 x) = x

63− ok1 (Left x) = refl

63+ ok1 (Left x) = Refl

64− ok1 (Right (Left x)) = refl

64+ ok1 (Right (Left x)) = Refl

65− ok1 (Right (Right x)) = refl

65+ ok1 (Right (Right x)) = Refl

66

67 ok2 : (x : Either (Either a b) c) -> eitherAssoc2 (eitherAssoc1 x) = x

68− ok2 (Left (Left x)) = refl

68+ ok2 (Left (Left x)) = Refl

69− ok2 (Left (Right x)) = refl

69+ ok2 (Left (Right x)) = Refl

70− ok2 (Right x) = refl

70+ ok2 (Right x) = Refl

71

72||| Disjunction with false is a no-op

73eitherBotLeft : Iso (Either _|_ a) a

@@ -78,10 +78,10 @@ eitherBotLeft = MkIso to from ok1 ok2

78 from : a -> Either _|_ a

79 from = Right

80 ok1 : (x : a) -> to (from x) = x

81− ok1 x = refl

81+ ok1 x = Refl

82 ok2 : (x : Either _|_ a) -> from (to x) = x

83 ok2 (Left x) = FalseElim x

84− ok2 (Right x) = refl

84+ ok2 (Right x) = Refl

85

86||| Disjunction with false is a no-op

87eitherBotRight : Iso (Either a _|_) a

@@ -119,7 +119,7 @@ pairComm = MkIso swap swap swapSwap swapSwap

119 swap (x, y) = (y, x)

120

121 swapSwap : (x : (a', b')) -> swap (swap x) = x

122− swapSwap (x, y) = refl

122+ swapSwap (x, y) = Refl

123

124||| Conjunction is associative

125pairAssoc : Iso (a, (b, c)) ((a, b), c)

@@ -130,15 +130,15 @@ pairAssoc = MkIso to from ok1 ok2

130 from : ((a, b), c) -> (a, (b, c))

131 from ((x, y), z) = (x, (y, z))

132 ok1 : (x : ((a, b), c)) -> to (from x) = x

133− ok1 ((x, y), z) = refl

133+ ok1 ((x, y), z) = Refl

134 ok2 : (x : (a, (b, c))) -> from (to x) = x

135− ok2 (x, (y, z)) = refl

135+ ok2 (x, (y, z)) = Refl

136

137||| Conjunction with truth is a no-op

138pairUnitRight : Iso (a, ()) a

139−pairUnitRight = MkIso fst (\x => (x, ())) (\x => refl) ok

139+pairUnitRight = MkIso fst (\x => (x, ())) (\x => Refl) ok

140 where ok : (x : (a, ())) -> (fst x, ()) = x

141− ok (x, ()) = refl

141+ ok (x, ()) = Refl

142

143||| Conjunction with truth is a no-op

144pairUnitLeft : Iso ((), a) a

@@ -165,11 +165,11 @@ pairCong {a = a} {a' = a'} {b = b} {b' = b'}

165 iso1 : (x : (a', b')) -> to'' (from'' x) = x

166 iso1 (x, y) = rewrite toFrom x in

167 rewrite toFrom' y in

168− refl

168+ Refl

169 iso2 : (x : (a, b)) -> from'' (to'' x) = x

170 iso2 (x, y) = rewrite fromTo x in

171 rewrite fromTo' y in

172− refl

172+ Refl

173

174||| Isomorphism is a congruence with regards to conjunction on the left

175pairCongLeft : Iso a a' -> Iso (a, b) (a', b)

@@ -190,11 +190,11 @@ distribLeft = MkIso to from toFrom fromTo

190 from (Left (x, y)) = (Left x, y)

191 from (Right (x, y)) = (Right x, y)

192 toFrom : (x : Either (a, c) (b, c)) -> to (from x) = x

193− toFrom (Left (x, y)) = refl

193+ toFrom (Left (x, y)) = Refl

194− toFrom (Right (x, y)) = refl

194+ toFrom (Right (x, y)) = Refl

195 fromTo : (x : (Either a b, c)) -> from (to x) = x

196− fromTo (Left x, y) = refl

196+ fromTo (Left x, y) = Refl

197− fromTo (Right x, y) = refl

197+ fromTo (Right x, y) = Refl

198

199||| Products distribute over sums

200distribRight : Iso (a, Either b c) (Either (a, b) (a, c))

@@ -217,10 +217,10 @@ step a iso1 iso2 = isoTrans iso1 iso2

217maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)

218maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2

219 where ok1 : (y : Maybe b) -> map to (map from y) = y

220− ok1 Nothing = refl

220+ ok1 Nothing = Refl

221 ok1 (Just x) = (Just (to (from x))) ={ cong (toFrom x) }= (Just x) QED

222 ok2 : (x : Maybe a) -> map from (map to x) = x

223− ok2 Nothing = refl

223+ ok2 Nothing = Refl

224 ok2 (Just x) = (Just (from (to x))) ={ cong (fromTo x) }= (Just x) QED

225

226||| `Maybe a` is the same as `Either a ()`

@@ -233,11 +233,11 @@ maybeEither = MkIso to from iso1 iso2

233 from (Left x) = Just x

234 from (Right ()) = Nothing

235 iso1 : (x : Either a ()) -> to (from x) = x

236− iso1 (Left x) = refl

236+ iso1 (Left x) = Refl

237− iso1 (Right ()) = refl

237+ iso1 (Right ()) = Refl

238 iso2 : (y : Maybe a) -> from (to y) = y

239− iso2 Nothing = refl

239+ iso2 Nothing = Refl

240− iso2 (Just x) = refl

240+ iso2 (Just x) = Refl

241

242||| Maybe of void is just unit

243maybeVoidUnit : Iso (Maybe _|_) ()

@@ -268,17 +268,17 @@ eitherMaybeRightMaybe {a} {b} =

268maybeIsoS : Iso (Maybe (Fin n)) (Fin (S n))

269maybeIsoS = MkIso forth back fb bf

270 where forth : Maybe (Fin n) -> Fin (S n)

271− forth Nothing = fZ

271+ forth Nothing = FZ

272− forth (Just x) = fS x

272+ forth (Just x) = FS x

273 back : Fin (S n) -> Maybe (Fin n)

274− back fZ = Nothing

274+ back FZ = Nothing

275− back (fS x) = Just x

275+ back (FS x) = Just x

276 bf : (x : Maybe (Fin n)) -> back (forth x) = x

277− bf Nothing = refl

277+ bf Nothing = Refl

278− bf (Just x) = refl

278+ bf (Just x) = Refl

279 fb : (y : Fin (S n)) -> forth (back y) = y

280− fb fZ = refl

280+ fb FZ = Refl

281− fb (fS x) = refl

281+ fb (FS x) = Refl

282

283finZeroBot : Iso (Fin 0) _|_

284finZeroBot = MkIso (\x => FalseElim (uninhabited x))

libs/base/Control/Isomorphism/Primitives.idr+4−4

@@ -20,16 +20,16 @@ integerIsoZZ = MkIso toZZ fromZZ fromToZZ toFromZZ

20 fromZZ n = cast n

21

22 toFromZZ : (n : Integer) -> fromZZ (toZZ n) = n

23− toFromZZ n = really_believe_me {a = n=n} {b = fromZZ (toZZ n) = n} refl

23+ toFromZZ n = really_believe_me {a = n=n} {b = fromZZ (toZZ n) = n} Refl

24

25 fromToZZ : (n : ZZ) -> toZZ (fromZZ n) = n

26− fromToZZ n = really_believe_me {a = n=n} {b = toZZ (fromZZ n) = n} refl

26+ fromToZZ n = really_believe_me {a = n=n} {b = toZZ (fromZZ n) = n} Refl

27

28

29packUnpackIso : Iso (List Char) String

30packUnpackIso = MkIso pack

31 unpack

32− (\str => really_believe_me {a = str=str} {b = pack (unpack str) = str} refl)

32+ (\str => really_believe_me {a = str=str} {b = pack (unpack str) = str} Refl)

33− (\cs => really_believe_me {a = cs=cs} {b = unpack (pack cs) = cs} refl)

33+ (\cs => really_believe_me {a = cs=cs} {b = unpack (pack cs) = cs} Refl)

34

35

libs/base/Data/Bits.idr+2−2

@@ -437,8 +437,8 @@ bitsToStr x = pack (helper last x)

437 where

438 %assert_total

439 helper : Fin (S n) -> Bits n -> List Char

440− helper fZ _ = []

440+ helper FZ _ = []

441− helper (fS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b

441+ helper (FS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b

442

443instance Show (Bits n) where

444 show = bitsToStr

libs/base/Data/BoundedList.idr+5−5

@@ -10,8 +10,8 @@ data BoundedList : Nat -> Type -> Type where

10

11||| Compute the length of a list.

12length : BoundedList n a -> Fin (S n)

13−length [] = fZ

13+length [] = FZ

14−length (x :: xs) = fS (length xs)

14+length (x :: xs) = FS (length xs)

15

16--------------------------------------------------------------------------------

17-- Indexing into bounded lists

@@ -19,8 +19,8 @@ length (x :: xs) = fS (length xs)

19

20index : Fin (S n) -> BoundedList n a -> Maybe a

21index _ [] = Nothing

22−index fZ (x :: _) = Just x

22+index FZ (x :: _) = Just x

23−index (fS f) (_ :: xs) = index f xs

23+index (FS f) (_ :: xs) = index f xs

24

25--------------------------------------------------------------------------------

26-- Adjusting bounds

@@ -90,5 +90,5 @@ pad {n=S n'} (x :: xs) padding = x :: pad {n=n'} xs padding

90--------------------------------------------------------------------------------

91

92zeroBoundIsEmpty : (xs : BoundedList 0 a) -> xs = the (BoundedList 0 a) []

93−zeroBoundIsEmpty [] = refl

93+zeroBoundIsEmpty [] = Refl

94zeroBoundIsEmpty (_ :: _) impossible

libs/base/Data/Buffer.idr+2−2

@@ -33,8 +33,8 @@ bitsFromNat Z = 0

33bitsFromNat (S k) = 1 + bitsFromNat k

34

35bitsFromFin : Fin n -> Bits64

36−bitsFromFin fZ = 0

36+bitsFromFin FZ = 0

37−bitsFromFin (fS k) = 1 + bitsFromFin k

37+bitsFromFin (FS k) = 1 + bitsFromFin k

38

39||| Allocate an empty Buffer. The size hint can be used to avoid

40||| unnecessary reallocations and copies under the hood if the

libs/base/Data/HVect.idr+9−9

@@ -13,22 +13,22 @@ data HVect : Vect k Type -> Type where

13

14||| Extract an element from an HVect

15index : (i : Fin k) -> HVect ts -> index i ts

16−index fZ (x::xs) = x

16+index FZ (x::xs) = x

17−index (fS j) (x::xs) = index j xs

17+index (FS j) (x::xs) = index j xs

18

19deleteAt : (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)

20−deleteAt fZ (x::xs) = xs

20+deleteAt FZ (x::xs) = xs

21−deleteAt {l = S m} (fS j) (x::xs) = x :: deleteAt j xs

21+deleteAt {l = S m} (FS j) (x::xs) = x :: deleteAt j xs

22−deleteAt {l = Z} (fS j) (x::xs) = absurd j

22+deleteAt {l = Z} (FS j) (x::xs) = absurd j

23deleteAt _ [] impossible

24

25replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts)

26−replaceAt fZ y (x::xs) = y::xs

26+replaceAt FZ y (x::xs) = y::xs

27−replaceAt (fS j) y (x::xs) = x :: replaceAt j y xs

27+replaceAt (FS j) y (x::xs) = x :: replaceAt j y xs

28

29updateAt : (i : Fin k) -> (index i ts -> t) -> HVect ts -> HVect (replaceAt i t ts)

30−updateAt fZ f (x::xs) = f x :: xs

30+updateAt FZ f (x::xs) = f x :: xs

31−updateAt (fS j) f (x::xs) = x :: updateAt j f xs

31+updateAt (FS j) f (x::xs) = x :: updateAt j f xs

32

33||| Append two `HVect`s.

34(++) : HVect ts -> HVect us -> HVect (ts ++ us)

libs/base/Data/Heap.idr+7−7

@@ -83,11 +83,11 @@ insert e = merge $ singleton e

83--------------------------------------------------------------------------------

84

85findMinimum : (h : MaxiphobicHeap a) -> (isEmpty h = False) -> a

86−findMinimum Empty refl impossible

86+findMinimum Empty Refl impossible

87findMinimum (Node s l e r) p = e

88

89deleteMinimum : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> MaxiphobicHeap a

90−deleteMinimum Empty refl impossible

90+deleteMinimum Empty Refl impossible

91deleteMinimum (Node s l e r) p = merge l r

92

93--------------------------------------------------------------------------------

@@ -96,7 +96,7 @@ deleteMinimum (Node s l e r) p = merge l r

96

97toList : Ord a => MaxiphobicHeap a -> List a

98toList Empty = []

99−toList (Node s l e r) = toList' (Node s l e r) refl

99+toList (Node s l e r) = toList' (Node s l e r) Refl

100 where

101 %assert_total -- relies on deleteMinimum making heap smaller

102 toList' : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> List a

@@ -143,20 +143,20 @@ absurdBoolDischarge p = replace {P = disjointTy} p ()

143 disjointTy True = _|_

144

145total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z

146−isEmptySizeZero Empty p = refl

146+isEmptySizeZero Empty p = Refl

147isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd

148

149total emptyHeapValid : Ord a => isValidHeap empty = True

150−emptyHeapValid = refl

150+emptyHeapValid = Refl

151

152total singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True

153−singletonHeapValid e = refl

153+singletonHeapValid e = Refl

154

155{-

156total mergePreservesValidHeaps : Ord a => (left : MaxiphobicHeap a) ->

157 (right : MaxiphobicHeap a) -> (leftValid : isValidHeap left = True) ->

158 (rightValid : isValidHeap right = True) -> isValidHeap $ merge left right = True

159−mergePreservesValidHeaps Empty Empty lp rp = refl

159+mergePreservesValidHeaps Empty Empty lp rp = Refl

160mergePreservesValidHeaps Empty (Node rs rl re rr) lp rp = rp

161mergePreservesValidHeaps (Node ls ll le lr) Empty lp rp = lp

162mergePreservesValidHeaps (Node ls ll le lr) (Node rs rl re rr) lp rp =

libs/base/Data/List.idr+2−2

@@ -18,7 +18,7 @@ instance Uninhabited (Elem {a} x []) where

18isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)

19isElem x [] = No absurd

20isElem x (y :: xs) with (decEq x y)

21− isElem x (x :: xs) | (Yes refl) = Yes Here

21+ isElem x (x :: xs) | (Yes Refl) = Yes Here

22 isElem x (y :: xs) | (No contra) with (isElem x xs)

23 isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)

24 isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)

@@ -26,5 +26,5 @@ isElem x (y :: xs) with (decEq x y)

26 mkNo : {xs' : List a} ->

27 ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) ->

28 Elem x' (y' :: xs') -> _|_

29− mkNo f g Here = f refl

29+ mkNo f g Here = f Refl

30 mkNo f g (There x) = g x

libs/base/Data/Vect.idr+2−2

@@ -20,14 +20,14 @@ noEmptyElem Here impossible

20

21||| An item not in the head and not in the tail is not in the Vect at all

22neitherHereNorThere : {x, y : a} -> {xs : Vect n a} -> Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))

23−neitherHereNorThere xneqy xninxs Here = xneqy refl

23+neitherHereNorThere xneqy xninxs Here = xneqy Refl

24neitherHereNorThere xneqy xninxs (There xinxs) = xninxs xinxs

25

26||| A decision procedure for Elem

27isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)

28isElem x [] = No noEmptyElem

29isElem x (y :: xs) with (decEq x y)

30− isElem x (x :: xs) | (Yes refl) = Yes Here

30+ isElem x (x :: xs) | (Yes Refl) = Yes Here

31 isElem x (y :: xs) | (No xneqy) with (isElem x xs)

32 isElem x (y :: xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)

33 isElem x (y :: xs) | (No xneqy) | (No xninxs) = No (neitherHereNorThere xneqy xninxs)

libs/base/Data/ZZ.idr+12−12

@@ -101,20 +101,20 @@ natMultZMult : (n : Nat) -> (m : Nat) -> (x : Nat)

101natMultZMult n m x h = cong h

102

103doubleNegElim : (z : ZZ) -> negZ (negZ z) = z

104−doubleNegElim (Pos Z) = refl

104+doubleNegElim (Pos Z) = Refl

105−doubleNegElim (Pos (S n)) = refl

105+doubleNegElim (Pos (S n)) = Refl

106−doubleNegElim (NegS Z) = refl

106+doubleNegElim (NegS Z) = Refl

107−doubleNegElim (NegS (S n)) = refl

107+doubleNegElim (NegS (S n)) = Refl

108

109-- Injectivity

110posInjective : Pos n = Pos m -> n = m

111−posInjective refl = refl

111+posInjective Refl = Refl

112

113negSInjective : NegS n = NegS m -> n = m

114−negSInjective refl = refl

114+negSInjective Refl = Refl

115

116posNotNeg : Pos n = NegS m -> _|_

117−posNotNeg refl impossible

117+posNotNeg Refl impossible

118

119-- Decidable equality

120instance DecEq ZZ where

@@ -129,16 +129,16 @@ instance DecEq ZZ where

129

130-- Plus

131plusZeroLeftNeutralZ : (right : ZZ) -> 0 + right = right

132−plusZeroLeftNeutralZ (Pos n) = refl

132+plusZeroLeftNeutralZ (Pos n) = Refl

133−plusZeroLeftNeutralZ (NegS n) = refl

133+plusZeroLeftNeutralZ (NegS n) = Refl

134

135plusZeroRightNeutralZ : (left : ZZ) -> left + 0 = left

136plusZeroRightNeutralZ (Pos n) = cong $ plusZeroRightNeutral n

137−plusZeroRightNeutralZ (NegS n) = refl

137+plusZeroRightNeutralZ (NegS n) = Refl

138

139plusCommutativeZ : (left : ZZ) -> (right : ZZ) -> (left + right = right + left)

140plusCommutativeZ (Pos n) (Pos m) = cong $ plusCommutative n m

141−plusCommutativeZ (Pos n) (NegS m) = refl

141+plusCommutativeZ (Pos n) (NegS m) = Refl

142−plusCommutativeZ (NegS n) (Pos m) = refl

142+plusCommutativeZ (NegS n) (Pos m) = Refl

143plusCommutativeZ (NegS n) (NegS m) = cong {f=NegS} $ cong {f=S} $ plusCommutative n m

144

libs/base/Decidable/Order.idr+55−66

@@ -48,7 +48,7 @@ maximum x y with (order x y)

48

49instance Preorder t ((=) {A = t} {B = t}) where

50 transitive a b c = trans {a = a} {b = b} {c = c}

51− reflexive a = refl

51+ reflexive a = Refl

52

53instance Equivalence t ((=) {A = t} {B = t}) where

54 symmetric a b prf = sym prf

@@ -60,99 +60,88 @@ instance Congruence t f ((=) {A = t} {B = t}) where

60-- Natural numbers

61--------------------------------------------------------------------------------

62

63−data NatLTE : Nat -> Nat -> Type where

63+total LTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->

64− nEqn : NatLTE n n

64+ LTE m n -> LTE n o ->

65− nLTESm : NatLTE n m -> NatLTE n (S m)

65+ LTE m o

66+LTEIsTransitive Z n o LTEZero nlteo = LTEZero

67+LTEIsTransitive (S m) (S n) (S o) (LTESucc mlten) (LTESucc nlteo) = LTESucc (LTEIsTransitive m n o mlten nlteo)

66

68

67−total NatLTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->

69+total LTEIsReflexive : (n : Nat) -> LTE n n

68− NatLTE m n -> NatLTE n o ->

70+LTEIsReflexive Z = LTEZero

69− NatLTE m o

71+LTEIsReflexive (S n) = LTESucc (LTEIsReflexive n)

70−NatLTEIsTransitive m n n mLTEn (nEqn) = mLTEn

71−NatLTEIsTransitive m n (S o) mLTEn (nLTESm nLTEo)

72− = nLTESm (NatLTEIsTransitive m n o mLTEn nLTEo)

73

72

74−total NatLTEIsReflexive : (n : Nat) -> NatLTE n n

73+instance Preorder Nat LTE where

75−NatLTEIsReflexive _ = nEqn

74+ transitive = LTEIsTransitive

75+ reflexive = LTEIsReflexive

76

77−instance Preorder Nat NatLTE where

77+total LTEIsAntisymmetric : (m : Nat) -> (n : Nat) ->

78− transitive = NatLTEIsTransitive

78+ LTE m n -> LTE n m -> m = n

79− reflexive = NatLTEIsReflexive

79+LTEIsAntisymmetric Z Z LTEZero LTEZero = Refl

80+LTEIsAntisymmetric (S n) (S m) (LTESucc mLTEn) (LTESucc nLTEm) with (LTEIsAntisymmetric n m mLTEn nLTEm)

81+ LTEIsAntisymmetric (S n) (S n) (LTESucc mLTEn) (LTESucc nLTEm) | Refl = Refl

80

82

81−total NatLTEIsAntisymmetric : (m : Nat) -> (n : Nat) ->

82− NatLTE m n -> NatLTE n m -> m = n

83−NatLTEIsAntisymmetric n n nEqn nEqn = refl

84−NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible

85−NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible

86−NatLTEIsAntisymmetric n m (nLTESm _) (nLTESm _) impossible

87

83

88−instance Poset Nat NatLTE where

84+instance Poset Nat LTE where

89− antisymmetric = NatLTEIsAntisymmetric

85+ antisymmetric = LTEIsAntisymmetric

90

86

91−total zeroNeverGreater : {n : Nat} -> NatLTE (S n) Z -> _|_

87+total zeroNeverGreater : {n : Nat} -> LTE (S n) Z -> _|_

92−zeroNeverGreater {n} (nLTESm _) impossible

88+zeroNeverGreater {n} LTEZero impossible

93−zeroNeverGreater {n} nEqn impossible

89+zeroNeverGreater {n} (LTESucc _) impossible

94

90

95−total zeroAlwaysSmaller : {n : Nat} -> NatLTE Z n

91+total zeroAlwaysSmaller : {n : Nat} -> LTE Z n

96−zeroAlwaysSmaller {n = Z } = nEqn

92+zeroAlwaysSmaller = LTEZero

97−zeroAlwaysSmaller {n = S k} = nLTESm (zeroAlwaysSmaller {n = k})

98

93

99−total

100−nGTSm : {n : Nat} -> {m : Nat} -> (NatLTE n m -> _|_) -> NatLTE n (S m) -> _|_

94+total ltesuccinjective : {n : Nat} -> {m : Nat} -> (LTE n m -> _|_) -> LTE (S n) (S m) -> _|_

101−nGTSm disprf (nLTESm nLTEm) = FalseElim (disprf nLTEm)

95+ltesuccinjective {n} {m} disprf (LTESucc nLTEm) = FalseElim (disprf nLTEm)

102−nGTSm {n} {m} disprf (nEqn) impossible

96+ltesuccinjective {n} {m} disprf LTEZero impossible

103

97

104−total

98+

105−decideNatLTE : (n : Nat) -> (m : Nat) -> Dec (NatLTE n m)

99+total decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTE n m)

106−decideNatLTE Z Z = Yes nEqn

100+decideLTE Z y = Yes LTEZero

107−decideNatLTE (S x) Z = No zeroNeverGreater

101+decideLTE (S x) Z = No zeroNeverGreater

108−decideNatLTE x (S y) with (decEq x (S y))

102+decideLTE (S x) (S y) with (decEq (S x) (S y))

109− | Yes eq = rewrite eq in Yes nEqn

103+ | Yes eq = rewrite eq in Yes (reflexive x)

110− | No _ with (decideNatLTE x y)

104+ | No _ with (decideLTE x y)

111− | Yes nLTEm = Yes (nLTESm nLTEm)

105+ | Yes nLTEm = Yes (LTESucc nLTEm)

112− | No nGTm = No (nGTSm nGTm)

106+ | No nGTm = No (ltesuccinjective nGTm)

113−

107+

114−instance Decidable [Nat,Nat] NatLTE where

108+instance Decidable [Nat,Nat] LTE where

115− decide = decideNatLTE

109+ decide = decideLTE

116

110

117total

111total

118−lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)

112+lte : (m : Nat) -> (n : Nat) -> Dec (LTE m n)

119−lte m n = decide {ts = [Nat,Nat]} {p = NatLTE} m n

113+lte m n = decide {ts = [Nat,Nat]} {p = LTE} m n

120

114

121total

115total

122−shift : (m : Nat) -> (n : Nat) -> NatLTE m n -> NatLTE (S m) (S n)

116+shift : (m : Nat) -> (n : Nat) -> LTE m n -> LTE (S m) (S n)

123−shift Z Z _ = nEqn

117+shift m n mLTEn = LTESucc mLTEn

124−shift Z (S Z) _ = nLTESm nEqn

118+

125−shift Z (S (S j)) _ = nLTESm (shift Z (S j) zeroAlwaysSmaller)

126−shift (S k) Z prf = FalseElim (zeroNeverGreater prf)

127−shift (S k) (S k) nEqn = nEqn

128−shift (S k) (S j) (nLTESm prf) = nLTESm (shift (S k) j prf)

129−

130−instance Ordered Nat NatLTE where

119+instance Ordered Nat LTE where

131− order Z n = Left zeroAlwaysSmaller

120+ order Z n = Left LTEZero

132− order m Z = Right zeroAlwaysSmaller

121+ order m Z = Right LTEZero

133 order (S k) (S j) with (order k j)

122 order (S k) (S j) with (order k j)

134 order (S k) (S j) | Left prf = Left (shift k j prf)

123 order (S k) (S j) | Left prf = Left (shift k j prf)

135 order (S k) (S j) | Right prf = Right (shift j k prf)

124 order (S k) (S j) | Right prf = Right (shift j k prf)

136

125

137−--------------------------------------------------------------------------------

126+----------------------------------------------------------------------------------

138−-- Finite numbers

127+---- Finite numbers

139−--------------------------------------------------------------------------------

128+----------------------------------------------------------------------------------

140

129

141using (k : Nat)

130using (k : Nat)

142 data FinLTE : Fin k -> Fin k -> Type where

131 data FinLTE : Fin k -> Fin k -> Type where

143− FromNatPrf : {m : Fin k} -> {n : Fin k} -> NatLTE (finToNat m) (finToNat n) -> FinLTE m n

132+ FromNatPrf : {m : Fin k} -> {n : Fin k} -> LTE (finToNat m) (finToNat n) -> FinLTE m n

144

133

145 instance Preorder (Fin k) FinLTE where

134 instance Preorder (Fin k) FinLTE where

146 transitive m n o (FromNatPrf p1) (FromNatPrf p2) =

135 transitive m n o (FromNatPrf p1) (FromNatPrf p2) =

147− FromNatPrf (NatLTEIsTransitive (finToNat m) (finToNat n) (finToNat o) p1 p2)

136+ FromNatPrf (LTEIsTransitive (finToNat m) (finToNat n) (finToNat o) p1 p2)

148− reflexive n = FromNatPrf (NatLTEIsReflexive (finToNat n))

137+ reflexive n = FromNatPrf (LTEIsReflexive (finToNat n))

149

138

150 instance Poset (Fin k) FinLTE where

139 instance Poset (Fin k) FinLTE where

151 antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =

140 antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =

152− finToNatInjective m n (NatLTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)

141+ finToNatInjective m n (LTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)

153

142

154 instance Decidable [Fin k, Fin k] FinLTE where

143 instance Decidable [Fin k, Fin k] FinLTE where

155− decide m n with (decideNatLTE (finToNat m) (finToNat n))

144+ decide m n with (decideLTE (finToNat m) (finToNat n))

156 | Yes prf = Yes (FromNatPrf prf)

145 | Yes prf = Yes (FromNatPrf prf)

157 | No disprf = No (\ (FromNatPrf prf) => disprf prf)

146 | No disprf = No (\ (FromNatPrf prf) => disprf prf)

158

147

libs/base/Syntax/PreorderReasoning.idr+3−3

@@ -1,6 +1,6 @@

1module Syntax.PreorderReasoning

2

3−-- QED is first to get the precedence to work out. It's just refl with an explicit argument.

3+-- QED is first to get the precedence to work out. It's just Refl with an explicit argument.

4syntax [expr] "QED" = qed expr

5-- foo ={ prf }= bar ={ prf' }= fnord QED

6-- is a proof that foo is related to fnord, with the intermediate step being bar, justified by prf and prf'

@@ -9,7 +9,7 @@ syntax [from] "={" [prf] "}=" [to] = step from prf to

9namespace Equal

10 using (a : Type, x : a, y : a, z : a)

11 qed : (x : a) -> x = x

12− qed x = the (x = x) refl

12+ qed x = the (x = x) Refl

13 step : (x : a) -> x = y -> (y = z) -> x = z

14− step x refl refl = refl

14+ step x Refl Refl = Refl

15

libs/base/System/Concurrency/Process.idr+13−13

@@ -12,38 +12,38 @@ data ProcID msg = MkPID Ptr

12||| Type safe message passing programs. Parameterised over the type of

13||| message which can be send, and the return type.

14data Process : (msgType : Type) -> Type -> Type where

15− lift : IO a -> Process msg a

15+ Lift : IO a -> Process msg a

16

17instance Functor (Process msg) where

18− map f (lift a) = lift (map f a)

18+ map f (Lift a) = Lift (map f a)

19

20instance Applicative (Process msg) where

21− pure = lift . return

21+ pure = Lift . return

22− (lift f) <$> (lift a) = lift (f <$> a)

22+ (Lift f) <$> (Lift a) = Lift (f <$> a)

23

24instance Monad (Process msg) where

25− (lift io) >>= k = lift (do x <- io

25+ (Lift io) >>= k = Lift (do x <- io

26 case k x of

27− lift v => v)

27+ Lift v => v)

28

29run : Process msg x -> IO x

30−run (lift prog) = prog

30+run (Lift prog) = prog

31

32||| Get current process ID

33myID : Process msg (ProcID msg)

34−myID = lift (return (MkPID prim__vm))

34+myID = Lift (return (MkPID prim__vm))

35

36||| Send a message to another process

37send : ProcID msg -> msg -> Process msg ()

38−send (MkPID p) m = lift (sendToThread p (prim__vm, m))

38+send (MkPID p) m = Lift (sendToThread p (prim__vm, m))

39

40||| Return whether a message is waiting in the queue

41msgWaiting : Process msg Bool

42−msgWaiting = lift checkMsgs

42+msgWaiting = Lift checkMsgs

43

44||| Receive a message - blocks if there is no message waiting

45recv : Process msg msg

46−recv {msg} = do (senderid, m) <- lift get

46+recv {msg} = do (senderid, m) <- Lift get

47 return m

48 where get : IO (Ptr, msg)

49 get = getMsg

@@ -51,11 +51,11 @@ recv {msg} = do (senderid, m) <- lift get

51||| receive a message, and return with the sender's process ID.

52recvWithSender : Process msg (ProcID msg, msg)

53recvWithSender {msg}

54− = do (senderid, m) <- lift get

54+ = do (senderid, m) <- Lift get

55 return (MkPID senderid, m)

56 where get : IO (Ptr, msg)

57 get = getMsg

58

59create : Process msg () -> Process msg (ProcID msg)

60−create (lift p) = do ptr <- lift (fork p)

60+create (Lift p) = do ptr <- Lift (fork p)

61 return (MkPID ptr)

libs/effects/Effect/Memory.idr+12−12

@@ -16,23 +16,23 @@ data RawMemory : Effect where

16 Free : RawMemory () (MemoryChunk n i) (\v => ())

17 Initialize : Bits8 ->

18 (size : Nat) ->

19− so (i + size <= n) ->

19+ So (i + size <= n) ->

20 RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (i + size))

21 Peek : (offset : Nat) ->

22 (size : Nat) ->

23− so (offset + size <= i) ->

23+ So (offset + size <= i) ->

24 RawMemory (Vect size Bits8)

25 (MemoryChunk n i) (\v => MemoryChunk n i)

26 Poke : (offset : Nat) ->

27 (Vect size Bits8) ->

28− so (offset <= i && offset + size <= n) ->

28+ So (offset <= i && offset + size <= n) ->

29 RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))

30 Move : (src : MemoryChunk src_size src_init) ->

31 (dst_offset : Nat) ->

32 (src_offset : Nat) ->

33 (size : Nat) ->

34− so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

34+ So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

35− so (src_offset + size <= src_init) ->

35+ So (src_offset + size <= src_init) ->

36 RawMemory () (MemoryChunk dst_size dst_init)

37 (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))

38 GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)

@@ -108,7 +108,7 @@ initialize : {i : Nat} ->

108 {n : Nat} ->

109 Bits8 ->

110 (size : Nat) ->

111− so (i + size <= n) ->

111+ So (i + size <= n) ->

112 Eff () [RAW_MEMORY (MemoryChunk n i)]

113 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])

114initialize c size prf = call $ Initialize c size prf

@@ -119,7 +119,7 @@ free = call Free

119peek : {i : Nat} ->

120 (offset : Nat) ->

121 (size : Nat) ->

122− so (offset + size <= i) ->

122+ So (offset + size <= i) ->

123 { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)

124peek offset size prf = call $ Peek offset size prf

125

@@ -127,7 +127,7 @@ poke : {n : Nat} ->

127 {i : Nat} ->

128 (offset : Nat) ->

129 Vect size Bits8 ->

130− so (offset <= i && offset + size <= n) ->

130+ So (offset <= i && offset + size <= n) ->

131 Eff () [RAW_MEMORY (MemoryChunk n i)]

132 (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])

133poke offset content prf = call $ Poke offset content prf

@@ -144,8 +144,8 @@ move' : {dst_size : Nat} ->

144 (dst_offset : Nat) ->

145 (src_offset : Nat) ->

146 (size : Nat) ->

147− so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

147+ So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

148− so (src_offset + size <= src_init) ->

148+ So (src_offset + size <= src_init) ->

149 Eff () [RAW_MEMORY (MemoryChunk dst_size dst_init)]

150 (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))])

151move' src_ptr dst_offset src_offset size dst_bounds src_bounds

@@ -160,8 +160,8 @@ move : {dst_size : Nat} ->

160 (dst_offset : Nat) ->

161 (src_offset : Nat) ->

162 (size : Nat) ->

163− so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

163+ So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

164− so (src_offset + size <= src_init) ->

164+ So (src_offset + size <= src_init) ->

165 Eff ()

166 [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)

167 , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]

libs/prelude/Builtins.idr+20−4

@@ -3,11 +3,27 @@

3%access public

4%default total

5

6+||| The canonical single-element type, also known as the trivially

7+||| true proposition.

8+%elim

9+ data Unit =

10+ ||| The trivial constructor for `()`.

11+ MkUnit

12+

13+||| The non-dependent pair type, also known as conjunction.

14+||| @A the type of the left elements in the pair

15+||| @B the type of the left elements in the pair

16+data Pair : (A : Type) -> (B : Type) -> Type where

17+ ||| A pair of elements

18+ ||| @a the left element of the pair

19+ ||| @b the right element of the pair

20+ MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B

21+

6||| Dependent pairs, in their internal representation

22||| Dependent pairs, in their internal representation

7||| @ a the type of the witness

23||| @ a the type of the witness

8||| @ P the type of the proof

24||| @ P the type of the proof

9data Sigma : (a : Type) -> (P : a -> Type) -> Type where

25data Sigma : (a : Type) -> (P : a -> Type) -> Type where

10− Sg_intro : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P

26+ MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P

11

27

12||| The eliminator for the empty type.

28||| The eliminator for the empty type.

13FalseElim : _|_ -> a

29FalseElim : _|_ -> a

@@ -32,15 +48,15 @@ infix 5 ~=~

32|||

48|||

33||| This is used by the `rewrite` tactic and term.

49||| This is used by the `rewrite` tactic and term.

34replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

50replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

35−replace refl prf = prf

51+replace Refl prf = prf

36

52

37||| Symmetry of propositional equality

53||| Symmetry of propositional equality

38sym : {l:a} -> {r:a} -> l = r -> r = l

54sym : {l:a} -> {r:a} -> l = r -> r = l

39−sym refl = refl

55+sym Refl = Refl

40

56

41||| Transitivity of propositional equality

57||| Transitivity of propositional equality

42trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c

58trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c

43−trans refl refl = refl

59+trans Refl Refl = Refl

44

60

45||| There are two types of laziness: that arising from lazy functions, and that

61||| There are two types of laziness: that arising from lazy functions, and that

46||| arising from codata. They differ in their totality condition.

62||| arising from codata. They differ in their totality condition.

libs/prelude/Decidable/Equality.idr+45−45

@@ -31,17 +31,17 @@ class DecEq t where

31--------------------------------------------------------------------------------

32

33instance DecEq () where

34− decEq () () = Yes refl

34+ decEq () () = Yes Refl

35

36--------------------------------------------------------------------------------

37-- Booleans

38--------------------------------------------------------------------------------

39total trueNotFalse : True = False -> _|_

40−trueNotFalse refl impossible

40+trueNotFalse Refl impossible

41

42instance DecEq Bool where

43− decEq True True = Yes refl

43+ decEq True True = Yes Refl

44− decEq False False = Yes refl

44+ decEq False False = Yes Refl

45 decEq True False = No trueNotFalse

46 decEq False True = No (negEqSym trueNotFalse)

47

@@ -50,10 +50,10 @@ instance DecEq Bool where

50--------------------------------------------------------------------------------

51

52total OnotS : Z = S n -> _|_

53−OnotS refl impossible

53+OnotS Refl impossible

54

55instance DecEq Nat where

56− decEq Z Z = Yes refl

56+ decEq Z Z = Yes Refl

57 decEq Z (S _) = No OnotS

58 decEq (S _) Z = No (negEqSym OnotS)

59 decEq (S n) (S m) with (decEq n m)

@@ -65,10 +65,10 @@ instance DecEq Nat where

65--------------------------------------------------------------------------------

66

67total nothingNotJust : {x : t} -> (Nothing {a = t} = Just x) -> _|_

68−nothingNotJust refl impossible

68+nothingNotJust Refl impossible

69

70instance (DecEq t) => DecEq (Maybe t) where

71− decEq Nothing Nothing = Yes refl

71+ decEq Nothing Nothing = Yes Refl

72 decEq (Just x') (Just y') with (decEq x' y')

73 | Yes p = Yes $ cong p

74 | No p = No $ \h : Just x' = Just y' => p $ justInjective h

@@ -80,7 +80,7 @@ instance (DecEq t) => DecEq (Maybe t) where

80--------------------------------------------------------------------------------

81

82total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> _|_

83−leftNotRight refl impossible

83+leftNotRight Refl impossible

84

85instance (DecEq a, DecEq b) => DecEq (Either a b) where

86 decEq (Left x') (Left y') with (decEq x' y')

@@ -96,40 +96,40 @@ instance (DecEq a, DecEq b) => DecEq (Either a b) where

96-- Fin

97--------------------------------------------------------------------------------

98

99−total fZNotfS : {f : Fin n} -> fZ {k = n} = fS f -> _|_

99+total FZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> _|_

100−fZNotfS refl impossible

100+FZNotFS Refl impossible

101

102instance DecEq (Fin n) where

103− decEq fZ fZ = Yes refl

103+ decEq FZ FZ = Yes Refl

104− decEq fZ (fS f) = No fZNotfS

104+ decEq FZ (FS f) = No FZNotFS

105− decEq (fS f) fZ = No $ negEqSym fZNotfS

105+ decEq (FS f) FZ = No $ negEqSym FZNotFS

106− decEq (fS f) (fS f') with (decEq f f')

106+ decEq (FS f) (FS f') with (decEq f f')

107 | Yes p = Yes $ cong p

108− | No p = No $ \h => p $ fSinjective {f = f} {f' = f'} h

108+ | No p = No $ \h => p $ FSinjective {f = f} {f' = f'} h

109

110--------------------------------------------------------------------------------

111-- Tuple

112--------------------------------------------------------------------------------

113

114lemma_both_neq : {x : a, y : b, x' : c, y' : d} -> (x = x' -> _|_) -> (y = y' -> _|_) -> ((x, y) = (x', y') -> _|_)

115−lemma_both_neq p_x_not_x' p_y_not_y' refl = p_x_not_x' refl

115+lemma_both_neq p_x_not_x' p_y_not_y' Refl = p_x_not_x' Refl

116

117lemma_snd_neq : {x : a, y : b, y' : d} -> (x = x) -> (y = y' -> _|_) -> ((x, y) = (x, y') -> _|_)

118−lemma_snd_neq refl p refl = p refl

118+lemma_snd_neq Refl p Refl = p Refl

119

120lemma_fst_neq_snd_eq : {x : a, x' : b, y : c, y' : d} ->

121 (x = x' -> _|_) ->

122 (y = y') ->

123 ((x, y) = (x', y) -> _|_)

124−lemma_fst_neq_snd_eq p_x_not_x' refl refl = p_x_not_x' refl

124+lemma_fst_neq_snd_eq p_x_not_x' Refl Refl = p_x_not_x' Refl

125

126instance (DecEq a, DecEq b) => DecEq (a, b) where

127 decEq (a, b) (a', b') with (decEq a a')

128− decEq (a, b) (a, b') | (Yes refl) with (decEq b b')

128+ decEq (a, b) (a, b') | (Yes Refl) with (decEq b b')

129− decEq (a, b) (a, b) | (Yes refl) | (Yes refl) = Yes refl

129+ decEq (a, b) (a, b) | (Yes Refl) | (Yes Refl) = Yes Refl

130− decEq (a, b) (a, b') | (Yes refl) | (No p) = No (\eq => lemma_snd_neq refl p eq)

130+ decEq (a, b) (a, b') | (Yes Refl) | (No p) = No (\eq => lemma_snd_neq Refl p eq)

131 decEq (a, b) (a', b') | (No p) with (decEq b b')

132− decEq (a, b) (a', b) | (No p) | (Yes refl) = No (\eq => lemma_fst_neq_snd_eq p refl eq)

132+ decEq (a, b) (a', b) | (No p) | (Yes Refl) = No (\eq => lemma_fst_neq_snd_eq p Refl eq)

133 decEq (a, b) (a', b') | (No p) | (No p') = No (\eq => lemma_both_neq p p' eq)

134

135

@@ -138,27 +138,27 @@ instance (DecEq a, DecEq b) => DecEq (a, b) where

138--------------------------------------------------------------------------------

139

140lemma_val_not_nil : {x : t, xs : List t} -> ((x :: xs) = Prelude.List.Nil {a = t} -> _|_)

141−lemma_val_not_nil refl impossible

141+lemma_val_not_nil Refl impossible

142

143lemma_x_eq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y) -> (xs = ys -> _|_) -> ((x :: xs) = (y :: ys) -> _|_)

144−lemma_x_eq_xs_neq refl p refl = p refl

144+lemma_x_eq_xs_neq Refl p Refl = p Refl

145

146lemma_x_neq_xs_eq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> _|_) -> (xs = ys) -> ((x :: xs) = (y :: ys) -> _|_)

147−lemma_x_neq_xs_eq p refl refl = p refl

147+lemma_x_neq_xs_eq p Refl Refl = p Refl

148

149lemma_x_neq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> _|_) -> (xs = ys -> _|_) -> ((x :: xs) = (y :: ys) -> _|_)

150−lemma_x_neq_xs_neq p p' refl = p refl

150+lemma_x_neq_xs_neq p p' Refl = p Refl

151

152instance DecEq a => DecEq (List a) where

153− decEq [] [] = Yes refl

153+ decEq [] [] = Yes Refl

154 decEq (x :: xs) [] = No lemma_val_not_nil

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

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

157− decEq (x :: xs) (x :: ys) | Yes refl with (decEq xs ys)

157+ decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)

158− decEq (x :: xs) (x :: xs) | (Yes refl) | (Yes refl) = Yes refl

158+ decEq (x :: xs) (x :: xs) | (Yes Refl) | (Yes Refl) = Yes Refl

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

159+ decEq (x :: xs) (x :: ys) | (Yes Refl) | (No p) = No (\eq => lemma_x_eq_xs_neq Refl p eq)

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

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

161+ decEq (x :: xs) (y :: xs) | (No p) | (Yes Refl) = No (\eq => lemma_x_neq_xs_eq p Refl eq)

162 decEq (x :: xs) (y :: ys) | (No p) | (No p') = No (\eq => lemma_x_neq_xs_neq p p' eq)

163

164

@@ -168,26 +168,26 @@ instance DecEq a => DecEq (List a) where

168

169total

170vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y

171−vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} refl = refl

171+vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl

172

173total

174vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys

175−vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} refl = refl

175+vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl

176

177instance DecEq a => DecEq (Vect n a) where

178− decEq [] [] = Yes refl

178+ decEq [] [] = Yes Refl

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

180− decEq (x :: xs) (x :: ys) | Yes refl with (decEq xs ys)

180+ decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)

181− decEq (x :: xs) (x :: xs) | Yes refl | Yes refl = Yes refl

181+ decEq (x :: xs) (x :: xs) | Yes Refl | Yes Refl = Yes Refl

182− decEq (x :: xs) (x :: ys) | Yes refl | No neq = No (neq . vectInjective2)

182+ decEq (x :: xs) (x :: ys) | Yes Refl | No neq = No (neq . vectInjective2)

183 decEq (x :: xs) (y :: ys) | No neq = No (neq . vectInjective1)

184

185{- The following definition is elaborated in a wrong case-tree. Examination pending.

186

187instance DecEq a => DecEq (Vect n a) where

188− decEq [] [] = Yes refl

188+ decEq [] [] = Yes Refl

189 decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)

190− decEq (x :: xs) (x :: xs) | (Yes refl, Yes refl) = Yes refl

190+ decEq (x :: xs) (x :: xs) | (Yes Refl, Yes Refl) = Yes Refl

191 decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))

192 decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))

193-}

@@ -202,7 +202,7 @@ instance DecEq a => DecEq (Vect n a) where

202instance DecEq Int where

203 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

204 where primitiveEq : x = y

205− primitiveEq = believe_me (refl {x})

205+ primitiveEq = believe_me (Refl {x})

206 postulate primitiveNotEq : x = y -> _|_

207

208--------------------------------------------------------------------------------

@@ -212,7 +212,7 @@ instance DecEq Int where

212instance DecEq Char where

213 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

214 where primitiveEq : x = y

215− primitiveEq = believe_me (refl {x})

215+ primitiveEq = believe_me (Refl {x})

216 postulate primitiveNotEq : x = y -> _|_

217

218--------------------------------------------------------------------------------

@@ -222,7 +222,7 @@ instance DecEq Char where

222instance DecEq Integer where

223 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

224 where primitiveEq : x = y

225− primitiveEq = believe_me (refl {x})

225+ primitiveEq = believe_me (Refl {x})

226 postulate primitiveNotEq : x = y -> _|_

227

228--------------------------------------------------------------------------------

@@ -232,7 +232,7 @@ instance DecEq Integer where

232instance DecEq Float where

233 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

234 where primitiveEq : x = y

235− primitiveEq = believe_me (refl {x})

235+ primitiveEq = believe_me (Refl {x})

236 postulate primitiveNotEq : x = y -> _|_

237

238--------------------------------------------------------------------------------

@@ -242,7 +242,7 @@ instance DecEq Float where

242instance DecEq String where

243 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

244 where primitiveEq : x = y

245− primitiveEq = believe_me (refl {x})

245+ primitiveEq = believe_me (Refl {x})

246 postulate primitiveNotEq : x = y -> _|_

247

248

libs/prelude/Prelude.idr+3−3

@@ -420,9 +420,9 @@ instance Enum Int where

420 go (x :: xs) = n + (cast x * inc) :: go xs

421

422instance Enum (Fin (S n)) where

423− pred fZ = fZ

423+ pred FZ = FZ

424− pred (fS n) = weaken n

424+ pred (FS n) = weaken n

425− succ n = case strengthen (fS n) of

425+ succ n = case strengthen (FS n) of

426 Left _ => last

427 Right k => k

428 toNat n = cast n

libs/prelude/Prelude/Basics.idr+3−1

@@ -1,5 +1,7 @@

1module Prelude.Basics

2

3+import Builtins

4+

3Not : Type -> Type

5Not : Type -> Type

4Not a = a -> _|_

6Not a = a -> _|_

5

7

@@ -42,7 +44,7 @@ apply f a = f a

42

44

43||| Equality is a congruence.

45||| Equality is a congruence.

44cong : {f : t -> u} -> (a = b) -> f a = f b

46cong : {f : t -> u} -> (a = b) -> f a = f b

45−cong refl = refl

47+cong Refl = Refl

46

48

47||| Decidability. A decidable property either holds or is a contradiction.

49||| Decidability. A decidable property either holds or is a contradiction.

48data Dec : Type -> Type where

50data Dec : Type -> Type where

libs/prelude/Prelude/Bool.idr+4−3

@@ -24,10 +24,11 @@ boolElim False t e = e

24||| If you find yourself using `so` for something other than primitive types,

25||| it may be appropriate to define a type of evidence for the property that you

26||| care about instead.

27−data so : Bool -> Type where oh : so True

27+data So : Bool -> Type where

28+ Oh : So True

28

29

29−instance Uninhabited (so False) where

30+instance Uninhabited (So False) where

30− uninhabited oh impossible

31+ uninhabited Oh impossible

31

32

32-- Syntactic sugar for boolean elimination.

33-- Syntactic sugar for boolean elimination.

33syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)

34syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)

libs/prelude/Prelude/Either.idr+6−6

@@ -30,10 +30,10 @@ isRight (Right r) = True

30-- Misc.

31--------------------------------------------------------------------------------

32

33−||| Perform a case analysis on a Boolean, providing clients with a `so` proof

33+||| Perform a case analysis on a Boolean, providing clients with a `So` proof

34−choose : (b : Bool) -> Either (so b) (so (not b))

34+choose : (b : Bool) -> Either (So b) (So (not b))

35−choose True = Left oh

35+choose True = Left Oh

36−choose False = Right oh

36+choose False = Right Oh

37

38||| Simply-typed eliminator for Either

39||| @ f the action to take on Left

@@ -97,9 +97,9 @@ instance (Eq a, Eq b) => Eq (Either a b) where

97||| Left is injective

98total leftInjective : {b : Type} -> {x : a} -> {y : a}

99 -> (Left {b = b} x = Left {b = b} y) -> (x = y)

100−leftInjective refl = refl

100+leftInjective Refl = Refl

101

102||| Right is injective

103total rightInjective : {a : Type} -> {x : b} -> {y : b}

104 -> (Right {a = a} x = Right {a = a} y) -> (x = y)

105−rightInjective refl = refl

105+rightInjective Refl = Refl

libs/prelude/Prelude/Fin.idr+44−44

@@ -12,39 +12,39 @@ import Prelude.Uninhabited

12||| exceedingly inefficient at run time.

13||| @ n the upper bound

14data Fin : (n : Nat) -> Type where

15− fZ : Fin (S k)

15+ FZ : Fin (S k)

16− fS : Fin k -> Fin (S k)

16+ FS : Fin k -> Fin (S k)

17

18instance Uninhabited (Fin Z) where

19− uninhabited fZ impossible

19+ uninhabited FZ impossible

20− uninhabited (fS f) impossible

20+ uninhabited (FS f) impossible

21

22−fSInjective : (m : Fin k) -> (n : Fin k) -> fS m = fS n -> m = n

22+FSInjective : (m : Fin k) -> (n : Fin k) -> FS m = FS n -> m = n

23−fSInjective left _ refl = refl

23+FSInjective left _ Refl = Refl

24

25instance Eq (Fin n) where

26− (==) fZ fZ = True

26+ (==) FZ FZ = True

27− (==) (fS k) (fS k') = k == k'

27+ (==) (FS k) (FS k') = k == k'

28 (==) _ _ = False

29

30||| There are no elements of `Fin Z`

31FinZAbsurd : Fin Z -> _|_

32−FinZAbsurd fZ impossible

32+FinZAbsurd FZ impossible

33

34FinZElim : Fin Z -> a

35FinZElim x = FalseElim (FinZAbsurd x)

36

37||| Convert a Fin to a Nat

38finToNat : Fin n -> Nat

39−finToNat fZ = Z

39+finToNat FZ = Z

40−finToNat (fS k) = S (finToNat k)

40+finToNat (FS k) = S (finToNat k)

41

42||| `finToNat` is injective

43finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn

44−finToNatInjective fZ fZ refl = refl

44+finToNatInjective FZ FZ Refl = Refl

45−finToNatInjective (fS m) fZ refl impossible

45+finToNatInjective (FS m) FZ Refl impossible

46−finToNatInjective fZ (fS n) refl impossible

46+finToNatInjective FZ (FS n) Refl impossible

47−finToNatInjective (fS m) (fS n) prf =

47+finToNatInjective (FS m) (FS n) prf =

48 cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))

49

50instance Cast (Fin n) Nat where

@@ -52,29 +52,29 @@ instance Cast (Fin n) Nat where

52

53||| Convert a Fin to an Integer

54finToInteger : Fin n -> Integer

55−finToInteger fZ = 0

55+finToInteger FZ = 0

56−finToInteger (fS k) = 1 + finToInteger k

56+finToInteger (FS k) = 1 + finToInteger k

57

58instance Cast (Fin n) Integer where

59 cast x = finToInteger x

60

61||| Weaken the bound on a Fin by 1

62weaken : Fin n -> Fin (S n)

63−weaken fZ = fZ

63+weaken FZ = FZ

64−weaken (fS k) = fS (weaken k)

64+weaken (FS k) = FS (weaken k)

65

66||| Weaken the bound on a Fin by some amount

67weakenN : (n : Nat) -> Fin m -> Fin (m + n)

68−weakenN n fZ = fZ

68+weakenN n FZ = FZ

69−weakenN n (fS f) = fS (weakenN n f)

69+weakenN n (FS f) = FS (weakenN n f)

70

71||| Attempt to tighten the bound on a Fin.

72||| Return `Left` if the bound could not be tightened, or `Right` if it could.

73strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)

74−strengthen {n = S k} fZ = Right fZ

74+strengthen {n = S k} FZ = Right FZ

75−strengthen {n = S k} (fS i) with (strengthen i)

75+strengthen {n = S k} (FS i) with (strengthen i)

76− strengthen (fS k) | Left x = Left (fS x)

76+ strengthen (FS k) | Left x = Left (FS x)

77− strengthen (fS k) | Right x = Right (fS x)

77+ strengthen (FS k) | Right x = Right (FS x)

78strengthen f = Left f

79

80||| Add some natural number to a Fin, extending the bound accordingly

@@ -82,24 +82,24 @@ strengthen f = Left f

82||| @ m the number to increase the Fin by

83shift : (m : Nat) -> Fin n -> Fin (m + n)

84shift Z f = f

85−shift {n=n} (S m) f = fS {k = (m + n)} (shift m f)

85+shift {n=n} (S m) f = FS {k = (m + n)} (shift m f)

86

87||| The largest element of some Fin type

88last : Fin (S n)

89−last {n=Z} = fZ

89+last {n=Z} = FZ

90−last {n=S _} = fS last

90+last {n=S _} = FS last

91

92−total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'

92+total FSinjective : {f : Fin n} -> {f' : Fin n} -> (FS f = FS f') -> f = f'

93−fSinjective refl = refl

93+FSinjective Refl = Refl

94

95instance Ord (Fin n) where

96− compare fZ fZ = EQ

96+ compare FZ FZ = EQ

97− compare fZ (fS _) = LT

97+ compare FZ (FS _) = LT

98− compare (fS _) fZ = GT

98+ compare (FS _) FZ = GT

99− compare (fS x) (fS y) = compare x y

99+ compare (FS x) (FS y) = compare x y

100

101instance MinBound (Fin (S n)) where

102− minBound = fZ

102+ minBound = FZ

103

104instance MaxBound (Fin (S n)) where

105 maxBound = last

@@ -107,28 +107,28 @@ instance MaxBound (Fin (S n)) where

107

108||| Add two Fins, extending the bound

109(+) : Fin n -> Fin m -> Fin (n + m)

110−(+) {n=S n} {m=m} fZ f' = rewrite plusCommutative n m in weaken (weakenN n f')

110+(+) {n=S n} {m=m} FZ f' = rewrite plusCommutative n m in weaken (weakenN n f')

111−(+) (fS f) f' = fS (f + f')

111+(+) (FS f) f' = FS (f + f')

112

113||| Substract two Fins, keeping the bound of the minuend

114(-) : Fin n -> Fin m -> Fin n

115−fZ - _ = fZ

115+FZ - _ = FZ

116−f - fZ = f

116+f - FZ = f

117−(fS f) - (fS f') = weaken $ f - f'

117+(FS f) - (FS f') = weaken $ f - f'

118

119||| Multiply two Fins, extending the bound

120(*) : Fin n -> Fin m -> Fin (n * m)

121(*) {n=Z} f f' = FinZElim f

122(*) {m=Z} f f' = FinZElim f'

123−(*) {n=S n} {m=S m} fZ f' = fZ

123+(*) {n=S n} {m=S m} FZ f' = FZ

124−(*) {n=S n} {m=S m} (fS f) f' = f' + (f * f')

124+(*) {n=S n} {m=S m} (FS f) f' = f' + (f * f')

125

126-- Construct a Fin from an integer literal which must fit in the given Fin

127

128natToFin : Nat -> (n : Nat) -> Maybe (Fin n)

129−natToFin Z (S j) = Just fZ

129+natToFin Z (S j) = Just FZ

130natToFin (S k) (S j) with (natToFin k j)

131− | Just k' = Just (fS k')

131+ | Just k' = Just (FS k')

132 | Nothing = Nothing

133natToFin _ _ = Nothing

134

libs/prelude/Prelude/List.idr+20−20

@@ -60,7 +60,7 @@ length (x::xs) = 1 + length xs

60index : (n : Nat) -> (l : List a) -> (ok : lt n (length l) = True) -> a

61index Z (x::xs) p = x

62index (S n) (x::xs) p = index n xs ?indexTailProof

63−index _ [] refl impossible

63+index _ [] Refl impossible

64

65||| Attempt to find a particular element of a list.

66|||

@@ -73,7 +73,7 @@ index' _ [] = Nothing

73||| Get the first element of a non-empty list

74||| @ ok proof that the list is non-empty

75head : (l : List a) -> {auto ok : isCons l = True} -> a

76−head [] {ok=refl} impossible

76+head [] {ok=Refl} impossible

77head (x::xs) {ok=p} = x

78

79||| Attempt to get the first element of a list. If the list is empty, return

@@ -85,7 +85,7 @@ head' (x::xs) = Just x

85||| Get the tail of a non-empty list.

86||| @ ok proof that the list is non-empty

87tail : (l : List a) -> {auto ok : isCons l = True} -> List a

88−tail [] {ok=refl} impossible

88+tail [] {ok=Refl} impossible

89tail (x::xs) {ok=p} = xs

90

91||| Attempt to get the tail of a list.

@@ -98,9 +98,9 @@ tail' (x::xs) = Just xs

98||| Retrieve the last element of a non-empty list.

99||| @ ok proof that the list is non-empty

100last : (l : List a) -> {auto ok : isCons l = True} -> a

101−last [] {ok=refl} impossible

101+last [] {ok=Refl} impossible

102last [x] {ok=p} = x

103−last (x::y::ys) {ok=p} = last (y::ys) {ok=refl}

103+last (x::y::ys) {ok=p} = last (y::ys) {ok=Refl}

104

105||| Attempt to retrieve the last element of a non-empty list.

106|||

@@ -115,9 +115,9 @@ last' (x::xs) =

115||| Return all but the last element of a non-empty list.

116||| @ ok proof that the list is non-empty

117init : (l : List a) -> {auto ok : isCons l = True} -> List a

118−init [] {ok=refl} impossible

118+init [] {ok=Refl} impossible

119init [x] {ok=p} = []

120−init (x::y::ys) {ok=p} = x :: init (y::ys) {ok=refl}

120+init (x::y::ys) {ok=p} = x :: init (y::ys) {ok=Refl}

121

122||| Attempt to Return all but the last element of a list.

123|||

@@ -251,8 +251,8 @@ instance Functor List where

251||| @ ok a proof that the lengths of the inputs are equal

252zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->

253 (ok : length l = length r) -> List c

254−zipWith f [] (y::ys) refl impossible

254+zipWith f [] (y::ys) Refl impossible

255−zipWith f (x::xs) [] refl impossible

255+zipWith f (x::xs) [] Refl impossible

256zipWith f [] [] p = []

257zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)

258

@@ -265,10 +265,10 @@ zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)

265||| @ ok' a proof that the lengths of the second and third inputs are equal

266zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->

267 (z : List c) -> (ok : length x = length y) -> (ok' : length y = length z) -> List d

268−zipWith3 f _ [] (z::zs) p refl impossible

268+zipWith3 f _ [] (z::zs) p Refl impossible

269−zipWith3 f _ (y::ys) [] p refl impossible

269+zipWith3 f _ (y::ys) [] p Refl impossible

270−zipWith3 f [] (y::ys) _ refl q impossible

270+zipWith3 f [] (y::ys) _ Refl q impossible

271−zipWith3 f (x::xs) [] _ refl q impossible

271+zipWith3 f (x::xs) [] _ Refl q impossible

272zipWith3 f [] [] [] p q = []

273zipWith3 f (x::xs) (y::ys) (z::zs) p q =

274 f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')

@@ -651,7 +651,7 @@ catMaybes (x::xs) =

651||| The empty list is a right identity for append.

652appendNilRightNeutral : (l : List a) ->

653 l ++ [] = l

654−appendNilRightNeutral [] = refl

654+appendNilRightNeutral [] = Refl

655appendNilRightNeutral (x::xs) =

656 let inductiveHypothesis = appendNilRightNeutral xs in

657 ?appendNilRightNeutralStepCase

@@ -659,7 +659,7 @@ appendNilRightNeutral (x::xs) =

659||| Appending lists is associative.

660appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->

661 l ++ (c ++ r) = (l ++ c) ++ r

662−appendAssociative [] c r = refl

662+appendAssociative [] c r = Refl

663appendAssociative (x::xs) c r =

664 let inductiveHypothesis = appendAssociative xs c r in

665 ?appendAssociativeStepCase

@@ -668,7 +668,7 @@ appendAssociative (x::xs) c r =

668||| of the input lists.

669lengthAppend : (left : List a) -> (right : List a) ->

670 length (left ++ right) = length left + length right

671−lengthAppend [] right = refl

671+lengthAppend [] right = Refl

672lengthAppend (x::xs) right =

673 let inductiveHypothesis = lengthAppend xs right in

674 ?lengthAppendStepCase

@@ -676,7 +676,7 @@ lengthAppend (x::xs) right =

676||| Mapping a function over a list doesn't change its length.

677mapPreservesLength : (f : a -> b) -> (l : List a) ->

678 length (map f l) = length l

679−mapPreservesLength f [] = refl

679+mapPreservesLength f [] = Refl

680mapPreservesLength f (x::xs) =

681 let inductiveHypothesis = mapPreservesLength f xs in

682 ?mapPreservesLengthStepCase

@@ -685,7 +685,7 @@ mapPreservesLength f (x::xs) =

685||| to appending them and then mapping the function.

686mapDistributesOverAppend : (f : a -> b) -> (l : List a) -> (r : List a) ->

687 map f (l ++ r) = map f l ++ map f r

688−mapDistributesOverAppend f [] r = refl

688+mapDistributesOverAppend f [] r = Refl

689mapDistributesOverAppend f (x::xs) r =

690 let inductiveHypothesis = mapDistributesOverAppend f xs r in

691 ?mapDistributesOverAppendStepCase

@@ -693,7 +693,7 @@ mapDistributesOverAppend f (x::xs) r =

693||| Mapping two functions is the same as mapping their composition.

694mapFusion : (f : b -> c) -> (g : a -> b) -> (l : List a) ->

695 map f (map g l) = map (f . g) l

696−mapFusion f g [] = refl

696+mapFusion f g [] = Refl

697mapFusion f g (x::xs) =

698 let inductiveHypothesis = mapFusion f g xs in

699 ?mapFusionStepCase

@@ -701,7 +701,7 @@ mapFusion f g (x::xs) =

701||| No list contains an element of the empty list by any predicate.

702hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->

703 hasAnyBy p [] l = False

704−hasAnyByNilFalse p [] = refl

704+hasAnyByNilFalse p [] = Refl

705hasAnyByNilFalse p (x::xs) =

706 let inductiveHypothesis = hasAnyByNilFalse p xs in

707 ?hasAnyByNilFalseStepCase

libs/prelude/Prelude/Maybe.idr+1−1

@@ -45,7 +45,7 @@ toMaybe True j = Just j

45toMaybe False j = Nothing

46

47justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y

48−justInjective refl = refl

48+justInjective Refl = Refl

49

50||| Convert a `Maybe a` value to an `a` value, using `neutral` in the case

51||| that the `Maybe` value is `Nothing`.

libs/prelude/Prelude/Nat.idr+107−107

@@ -22,7 +22,7 @@ import Prelude.Uninhabited

22%name Nat k,j,i,n,m

23

24instance Uninhabited (Z = S n) where

25− uninhabited refl impossible

25+ uninhabited Refl impossible

26

27--------------------------------------------------------------------------------

28-- Syntactic tests

@@ -94,9 +94,9 @@ hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)

94||| @ m the larger number

95data LTE : (n, m : Nat) -> Type where

96 ||| Zero is the smallest Nat

97− lteZero : LTE Z right

97+ LTEZero : LTE Z right

98 ||| If n <= m, then n + 1 <= m + 1

99− lteSucc : LTE left right -> LTE (S left) (S right)

99+ LTESucc : LTE left right -> LTE (S left) (S right)

100

101||| Greater than or equal to

102total GTE : Nat -> Nat -> Type

@@ -112,18 +112,18 @@ GT left right = LT right left

112

113||| A successor is never less than or equal zero

114succNotLTEzero : Not (S m `LTE` Z)

115−succNotLTEzero lteZero impossible

115+succNotLTEzero LTEZero impossible

116

117||| If two numbers are ordered, their predecessors are too

118fromLteSucc : (S m `LTE` S n) -> (m `LTE` n)

119−fromLteSucc (lteSucc x) = x

119+fromLteSucc (LTESucc x) = x

120

121||| A decision procedure for `LTE`

122isLTE : (m, n : Nat) -> Dec (m `LTE` n)

123−isLTE Z n = Yes lteZero

123+isLTE Z n = Yes LTEZero

124isLTE (S k) Z = No succNotLTEzero

125isLTE (S k) (S j) with (isLTE k j)

126− isLTE (S k) (S j) | (Yes prf) = Yes (lteSucc prf)

126+ isLTE (S k) (S j) | (Yes prf) = Yes (LTESucc prf)

127 isLTE (S k) (S j) | (No contra) = No (contra . fromLteSucc)

128

129||| Boolean test than one Nat is less than or equal to another

@@ -329,18 +329,18 @@ lcm x y = divNat (x * y) (gcd x y)

329-- An informative comparison view

330--------------------------------------------------------------------------------

331data CmpNat : Nat -> Nat -> Type where

332− cmpLT : (y : _) -> CmpNat x (x + S y)

332+ CmpLT : (y : _) -> CmpNat x (x + S y)

333− cmpEQ : CmpNat x x

333+ CmpEQ : CmpNat x x

334− cmpGT : (x : _) -> CmpNat (y + S x) y

334+ CmpGT : (x : _) -> CmpNat (y + S x) y

335

336total cmp : (x, y : Nat) -> CmpNat x y

337−cmp Z Z = cmpEQ

337+cmp Z Z = CmpEQ

338−cmp Z (S k) = cmpLT _

338+cmp Z (S k) = CmpLT _

339−cmp (S k) Z = cmpGT _

339+cmp (S k) Z = CmpGT _

340cmp (S x) (S y) with (cmp x y)

341− cmp (S x) (S (x + (S k))) | cmpLT k = cmpLT k

341+ cmp (S x) (S (x + (S k))) | CmpLT k = CmpLT k

342− cmp (S x) (S x) | cmpEQ = cmpEQ

342+ cmp (S x) (S x) | CmpEQ = CmpEQ

343− cmp (S (y + (S k))) (S y) | cmpGT k = cmpGT k

343+ cmp (S (y + (S k))) (S y) | CmpGT k = CmpGT k

344

345--------------------------------------------------------------------------------

346-- Properties

@@ -351,26 +351,26 @@ cmp (S x) (S y) with (cmp x y)

351||| S preserves equality

352total eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->

353 S left = S right

354−eqSucc left _ refl = refl

354+eqSucc left _ Refl = Refl

355

356||| S is injective

357total succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->

358 left = right

359−succInjective left _ refl = refl

359+succInjective left _ Refl = Refl

360

361-- Plus

362total plusZeroLeftNeutral : (right : Nat) -> 0 + right = right

363−plusZeroLeftNeutral right = refl

363+plusZeroLeftNeutral right = Refl

364

365total plusZeroRightNeutral : (left : Nat) -> left + 0 = left

366−plusZeroRightNeutral Z = refl

366+plusZeroRightNeutral Z = Refl

367plusZeroRightNeutral (S n) =

368 let inductiveHypothesis = plusZeroRightNeutral n in

369 ?plusZeroRightNeutralStepCase

370

371total plusSuccRightSucc : (left : Nat) -> (right : Nat) ->

372 S (left + right) = left + (S right)

373−plusSuccRightSucc Z right = refl

373+plusSuccRightSucc Z right = Refl

374plusSuccRightSucc (S left) right =

375 let inductiveHypothesis = plusSuccRightSucc left right in

376 ?plusSuccRightSuccStepCase

@@ -384,21 +384,21 @@ plusCommutative (S left) right =

384

385total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

386 left + (centre + right) = (left + centre) + right

387−plusAssociative Z centre right = refl

387+plusAssociative Z centre right = Refl

388plusAssociative (S left) centre right =

389 let inductiveHypothesis = plusAssociative left centre right in

390 ?plusAssociativeStepCase

391

392total plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->

393 (p : left = right) -> left + c = right + c

394−plusConstantRight left _ c refl = refl

394+plusConstantRight left _ c Refl = Refl

395

396total plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->

397 (p : left = right) -> c + left = c + right

398−plusConstantLeft left _ c refl = refl

398+plusConstantLeft left _ c Refl = Refl

399

400total plusOneSucc : (right : Nat) -> 1 + right = S right

401−plusOneSucc n = refl

401+plusOneSucc n = Refl

402

403total plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->

404 (p : left + right = left + right') -> right = right'

@@ -423,24 +423,24 @@ plusLeftLeftRightZero (S left) right p =

423

424-- Mult

425total multZeroLeftZero : (right : Nat) -> Z * right = Z

426−multZeroLeftZero right = refl

426+multZeroLeftZero right = Refl

427

428total multZeroRightZero : (left : Nat) -> left * Z = Z

429−multZeroRightZero Z = refl

429+multZeroRightZero Z = Refl

430multZeroRightZero (S left) =

431 let inductiveHypothesis = multZeroRightZero left in

432 ?multZeroRightZeroStepCase

433

434total multRightSuccPlus : (left : Nat) -> (right : Nat) ->

435 left * (S right) = left + (left * right)

436−multRightSuccPlus Z right = refl

436+multRightSuccPlus Z right = Refl

437multRightSuccPlus (S left) right =

438 let inductiveHypothesis = multRightSuccPlus left right in

439 ?multRightSuccPlusStepCase

440

441total multLeftSuccPlus : (left : Nat) -> (right : Nat) ->

442 (S left) * right = right + (left * right)

443−multLeftSuccPlus left right = refl

443+multLeftSuccPlus left right = Refl

444

445total multCommutative : (left : Nat) -> (right : Nat) ->

446 left * right = right * left

@@ -451,33 +451,33 @@ multCommutative (S left) right =

451

452total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

453 left * (centre + right) = (left * centre) + (left * right)

454−multDistributesOverPlusRight Z centre right = refl

454+multDistributesOverPlusRight Z centre right = Refl

455multDistributesOverPlusRight (S left) centre right =

456 let inductiveHypothesis = multDistributesOverPlusRight left centre right in

457 ?multDistributesOverPlusRightStepCase

458

459total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

460 (left + centre) * right = (left * right) + (centre * right)

461−multDistributesOverPlusLeft Z centre right = refl

461+multDistributesOverPlusLeft Z centre right = Refl

462multDistributesOverPlusLeft (S left) centre right =

463 let inductiveHypothesis = multDistributesOverPlusLeft left centre right in

464 ?multDistributesOverPlusLeftStepCase

465

466total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

467 left * (centre * right) = (left * centre) * right

468−multAssociative Z centre right = refl

468+multAssociative Z centre right = Refl

469multAssociative (S left) centre right =

470 let inductiveHypothesis = multAssociative left centre right in

471 ?multAssociativeStepCase

472

473total multOneLeftNeutral : (right : Nat) -> 1 * right = right

474−multOneLeftNeutral Z = refl

474+multOneLeftNeutral Z = Refl

475multOneLeftNeutral (S right) =

476 let inductiveHypothesis = multOneLeftNeutral right in

477 ?multOneLeftNeutralStepCase

478

479total multOneRightNeutral : (left : Nat) -> left * 1 = left

480−multOneRightNeutral Z = refl

480+multOneRightNeutral Z = Refl

481multOneRightNeutral (S left) =

482 let inductiveHypothesis = multOneRightNeutral left in

483 ?multOneRightNeutralStepCase

@@ -485,53 +485,53 @@ multOneRightNeutral (S left) =

485-- Minus

486total minusSuccSucc : (left : Nat) -> (right : Nat) ->

487 (S left) - (S right) = left - right

488−minusSuccSucc left right = refl

488+minusSuccSucc left right = Refl

489

490total minusZeroLeft : (right : Nat) -> 0 - right = Z

491−minusZeroLeft right = refl

491+minusZeroLeft right = Refl

492

493total minusZeroRight : (left : Nat) -> left - 0 = left

494−minusZeroRight Z = refl

494+minusZeroRight Z = Refl

495−minusZeroRight (S left) = refl

495+minusZeroRight (S left) = Refl

496

497total minusZeroN : (n : Nat) -> Z = n - n

498−minusZeroN Z = refl

498+minusZeroN Z = Refl

499minusZeroN (S n) = minusZeroN n

500

501total minusOneSuccN : (n : Nat) -> S Z = (S n) - n

502−minusOneSuccN Z = refl

502+minusOneSuccN Z = Refl

503minusOneSuccN (S n) = minusOneSuccN n

504

505total minusSuccOne : (n : Nat) -> S n - 1 = n

506−minusSuccOne Z = refl

506+minusSuccOne Z = Refl

507−minusSuccOne (S n) = refl

507+minusSuccOne (S n) = Refl

508

509total minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = Z

510−minusPlusZero Z m = refl

510+minusPlusZero Z m = Refl

511minusPlusZero (S n) m = minusPlusZero n m

512

513total minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

514 left - centre - right = left - (centre + right)

515−minusMinusMinusPlus Z Z right = refl

515+minusMinusMinusPlus Z Z right = Refl

516−minusMinusMinusPlus (S left) Z right = refl

516+minusMinusMinusPlus (S left) Z right = Refl

517−minusMinusMinusPlus Z (S centre) right = refl

517+minusMinusMinusPlus Z (S centre) right = Refl

518minusMinusMinusPlus (S left) (S centre) right =

519 let inductiveHypothesis = minusMinusMinusPlus left centre right in

520 ?minusMinusMinusPlusStepCase

521

522total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->

523 (left + right) - (left + right') = right - right'

524−plusMinusLeftCancel Z right right' = refl

524+plusMinusLeftCancel Z right right' = Refl

525plusMinusLeftCancel (S left) right right' =

526 let inductiveHypothesis = plusMinusLeftCancel left right right' in

527 ?plusMinusLeftCancelStepCase

528

529total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

530 (left - centre) * right = (left * right) - (centre * right)

531−multDistributesOverMinusLeft Z Z right = refl

531+multDistributesOverMinusLeft Z Z right = Refl

532multDistributesOverMinusLeft (S left) Z right =

533 ?multDistributesOverMinusLeftBaseCase

534−multDistributesOverMinusLeft Z (S centre) right = refl

534+multDistributesOverMinusLeft Z (S centre) right = Refl

535multDistributesOverMinusLeft (S left) (S centre) right =

536 let inductiveHypothesis = multDistributesOverMinusLeft left centre right in

537 ?multDistributesOverMinusLeftStepCase

@@ -544,7 +544,7 @@ multDistributesOverMinusRight left centre right =

544-- Power

545total powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =

546 base * (power base exp)

547−powerSuccPowerLeft base exp = refl

547+powerSuccPowerLeft base exp = Refl

548

549total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->

550 (power base exp) * (power base exp') = power base (exp + exp')

@@ -554,22 +554,22 @@ multPowerPowerPlus base (S exp) exp' =

554 ?multPowerPowerPlusStepCase

555

556total powerZeroOne : (base : Nat) -> power base 0 = S Z

557−powerZeroOne base = refl

557+powerZeroOne base = Refl

558

559total powerOneNeutral : (base : Nat) -> power base 1 = base

560−powerOneNeutral Z = refl

560+powerOneNeutral Z = Refl

561powerOneNeutral (S base) =

562 let inductiveHypothesis = powerOneNeutral base in

563 ?powerOneNeutralStepCase

564

565total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z

566−powerOneSuccOne Z = refl

566+powerOneSuccOne Z = Refl

567powerOneSuccOne (S exp) =

568 let inductiveHypothesis = powerOneSuccOne exp in

569 ?powerOneSuccOneStepCase

570

571total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base

572−powerSuccSuccMult Z = refl

572+powerSuccSuccMult Z = Refl

573powerSuccSuccMult (S base) =

574 let inductiveHypothesis = powerSuccSuccMult base in

575 ?powerSuccSuccMultStepCase

@@ -583,11 +583,11 @@ powerPowerMultPower base exp (S exp') =

583

584-- Pred

585total predSucc : (n : Nat) -> pred (S n) = n

586−predSucc n = refl

586+predSucc n = Refl

587

588total minusSuccPred : (left : Nat) -> (right : Nat) ->

589 left - (S right) = pred (left - right)

590−minusSuccPred Z right = refl

590+minusSuccPred Z right = Refl

591minusSuccPred (S left) Z =

592 let inductiveHypothesis = minusSuccPred left Z in

593 ?minusSuccPredStepCase

@@ -598,125 +598,125 @@ minusSuccPred (S left) (S right) =

598-- boolElim

599total boolElimSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->

600 S (boolElim cond t f) = boolElim cond (S t) (S f)

601−boolElimSuccSucc True t f = refl

601+boolElimSuccSucc True t f = Refl

602−boolElimSuccSucc False t f = refl

602+boolElimSuccSucc False t f = Refl

603

604total boolElimPlusPlusLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->

605 left + (boolElim cond t f) = boolElim cond (left + t) (left + f)

606−boolElimPlusPlusLeft True left t f = refl

606+boolElimPlusPlusLeft True left t f = Refl

607−boolElimPlusPlusLeft False left t f = refl

607+boolElimPlusPlusLeft False left t f = Refl

608

609total boolElimPlusPlusRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->

610 (boolElim cond t f) + right = boolElim cond (t + right) (f + right)

611−boolElimPlusPlusRight True right t f = refl

611+boolElimPlusPlusRight True right t f = Refl

612−boolElimPlusPlusRight False right t f = refl

612+boolElimPlusPlusRight False right t f = Refl

613

614total boolElimMultMultLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->

615 left * (boolElim cond t f) = boolElim cond (left * t) (left * f)

616−boolElimMultMultLeft True left t f = refl

616+boolElimMultMultLeft True left t f = Refl

617−boolElimMultMultLeft False left t f = refl

617+boolElimMultMultLeft False left t f = Refl

618

619total boolElimMultMultRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->

620 (boolElim cond t f) * right = boolElim cond (t * right) (f * right)

621−boolElimMultMultRight True right t f = refl

621+boolElimMultMultRight True right t f = Refl

622−boolElimMultMultRight False right t f = refl

622+boolElimMultMultRight False right t f = Refl

623

624-- Orders

625total lteNTrue : (n : Nat) -> lte n n = True

626−lteNTrue Z = refl

626+lteNTrue Z = Refl

627lteNTrue (S n) = lteNTrue n

628

629−total lteSuccZeroFalse : (n : Nat) -> lte (S n) Z = False

629+total LTESuccZeroFalse : (n : Nat) -> lte (S n) Z = False

630−lteSuccZeroFalse Z = refl

630+LTESuccZeroFalse Z = Refl

631−lteSuccZeroFalse (S n) = refl

631+LTESuccZeroFalse (S n) = Refl

632

633-- Minimum and maximum

634total maximumAssociative : (l,c,r : Nat) -> maximum l (maximum c r) = maximum (maximum l c) r

635−maximumAssociative Z c r = refl

635+maximumAssociative Z c r = Refl

636−maximumAssociative (S k) Z r = refl

636+maximumAssociative (S k) Z r = Refl

637−maximumAssociative (S k) (S j) Z = refl

637+maximumAssociative (S k) (S j) Z = Refl

638−maximumAssociative (S k) (S j) (S i) = rewrite maximumAssociative k j i in refl

638+maximumAssociative (S k) (S j) (S i) = rewrite maximumAssociative k j i in Refl

639

640total maximumCommutative : (l, r : Nat) -> maximum l r = maximum r l

641−maximumCommutative Z Z = refl

641+maximumCommutative Z Z = Refl

642−maximumCommutative Z (S k) = refl

642+maximumCommutative Z (S k) = Refl

643−maximumCommutative (S k) Z = refl

643+maximumCommutative (S k) Z = Refl

644−maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in refl

644+maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in Refl

645

646total maximumIdempotent : (n : Nat) -> maximum n n = n

647−maximumIdempotent Z = refl

647+maximumIdempotent Z = Refl

648maximumIdempotent (S k) = cong (maximumIdempotent k)

649

650total minimumAssociative : (l,c,r : Nat) -> minimum l (minimum c r) = minimum (minimum l c) r

651−minimumAssociative Z c r = refl

651+minimumAssociative Z c r = Refl

652−minimumAssociative (S k) Z r = refl

652+minimumAssociative (S k) Z r = Refl

653−minimumAssociative (S k) (S j) Z = refl

653+minimumAssociative (S k) (S j) Z = Refl

654−minimumAssociative (S k) (S j) (S i) = rewrite minimumAssociative k j i in refl

654+minimumAssociative (S k) (S j) (S i) = rewrite minimumAssociative k j i in Refl

655

656total minimumCommutative : (l, r : Nat) -> minimum l r = minimum r l

657−minimumCommutative Z Z = refl

657+minimumCommutative Z Z = Refl

658−minimumCommutative Z (S k) = refl

658+minimumCommutative Z (S k) = Refl

659−minimumCommutative (S k) Z = refl

659+minimumCommutative (S k) Z = Refl

660−minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in refl

660+minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in Refl

661

662total minimumIdempotent : (n : Nat) -> minimum n n = n

663−minimumIdempotent Z = refl

663+minimumIdempotent Z = Refl

664minimumIdempotent (S k) = cong (minimumIdempotent k)

665

666total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z

667−minimumZeroZeroRight Z = refl

667+minimumZeroZeroRight Z = Refl

668minimumZeroZeroRight (S right) = minimumZeroZeroRight right

669

670total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z

671−minimumZeroZeroLeft Z = refl

671+minimumZeroZeroLeft Z = Refl

672−minimumZeroZeroLeft (S left) = refl

672+minimumZeroZeroLeft (S left) = Refl

673

674total minimumSuccSucc : (left : Nat) -> (right : Nat) ->

675 minimum (S left) (S right) = S (minimum left right)

676−minimumSuccSucc Z Z = refl

676+minimumSuccSucc Z Z = Refl

677−minimumSuccSucc (S left) Z = refl

677+minimumSuccSucc (S left) Z = Refl

678−minimumSuccSucc Z (S right) = refl

678+minimumSuccSucc Z (S right) = Refl

679minimumSuccSucc (S left) (S right) =

680 let inductiveHypothesis = minimumSuccSucc left right in

681 ?minimumSuccSuccStepCase

682

683total maximumZeroNRight : (right : Nat) -> maximum Z right = right

684−maximumZeroNRight Z = refl

684+maximumZeroNRight Z = Refl

685−maximumZeroNRight (S right) = refl

685+maximumZeroNRight (S right) = Refl

686

687total maximumZeroNLeft : (left : Nat) -> maximum left Z = left

688−maximumZeroNLeft Z = refl

688+maximumZeroNLeft Z = Refl

689−maximumZeroNLeft (S left) = refl

689+maximumZeroNLeft (S left) = Refl

690

691total maximumSuccSucc : (left : Nat) -> (right : Nat) ->

692 S (maximum left right) = maximum (S left) (S right)

693−maximumSuccSucc Z Z = refl

693+maximumSuccSucc Z Z = Refl

694−maximumSuccSucc (S left) Z = refl

694+maximumSuccSucc (S left) Z = Refl

695−maximumSuccSucc Z (S right) = refl

695+maximumSuccSucc Z (S right) = Refl

696maximumSuccSucc (S left) (S right) =

697 let inductiveHypothesis = maximumSuccSucc left right in

698 ?maximumSuccSuccStepCase

699

700total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)

701−sucMaxL Z = refl

701+sucMaxL Z = Refl

702sucMaxL (S l) = cong (sucMaxL l)

703

704total sucMaxR : (l : Nat) -> maximum l (S l) = (S l)

705−sucMaxR Z = refl

705+sucMaxR Z = Refl

706sucMaxR (S l) = cong (sucMaxR l)

707

708total sucMinL : (l : Nat) -> minimum (S l) l = l

709−sucMinL Z = refl

709+sucMinL Z = Refl

710sucMinL (S l) = cong (sucMinL l)

711

712total sucMinR : (l : Nat) -> minimum l (S l) = l

713−sucMinR Z = refl

713+sucMinR Z = Refl

714sucMinR (S l) = cong (sucMinR l)

715

716-- div and mod

717total modZeroZero : (n : Nat) -> mod 0 n = Z

718−modZeroZero Z = refl

718+modZeroZero Z = Refl

719−modZeroZero (S n) = refl

719+modZeroZero (S n) = Refl

720

721--------------------------------------------------------------------------------

722-- Proofs

libs/prelude/Prelude/Pairs.idr+6−6

@@ -9,27 +9,27 @@ using (a : Type, P : a -> Type)

9

10 ||| Dependent pair where the first field is erased.

11 data Exists : (P : a -> Type) -> Type where

12− evidence : .(x : a) -> (pf : P x) -> Exists P

12+ Evidence : .(x : a) -> (pf : P x) -> Exists P

13

14 ||| Dependent pair where the second field is erased.

15 data Subset : (a : Type) -> (P : a -> Type) -> Type where

16− element : (x : a) -> .(pf : P x) -> Subset a P

16+ Element : (x : a) -> .(pf : P x) -> Subset a P

17

18 -- Monomorphic projections

19

20 namespace Exists

21 getWitness : Exists {a} P -> a

22− getWitness (evidence x pf) = x

22+ getWitness (Evidence x pf) = x

23

24 getProof : (x : Exists {a} P) -> P (getWitness x)

25− getProof (evidence x pf) = pf

25+ getProof (Evidence x pf) = pf

26

27 namespace Subset

28 getWitness : Subset a P -> a

29− getWitness (element x pf) = x

29+ getWitness (Element x pf) = x

30

31 getProof : (x : Subset a P) -> P (getWitness x)

32− getProof (element x pf) = pf

32+ getProof (Element x pf) = pf

33

34 namespace Sigma

35 getWitness : Sigma a P -> a

libs/prelude/Prelude/Strings.idr+2−2

@@ -74,11 +74,11 @@ data StrM : String -> Type where

74 StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)

75

76||| Version of 'strHead' that statically verifies that the string is not empty.

77−strHead' : (x : String) -> so (not (x == "")) -> Char

77+strHead' : (x : String) -> So (not (x == "")) -> Char

78strHead' x p = assert_total $ prim__strHead x

79

80||| Version of 'strTail' that statically verifies that the string is not empty.

81−strTail' : (x : String) -> so (not (x == "")) -> String

81+strTail' : (x : String) -> So (not (x == "")) -> String

82strTail' x p = assert_total $ prim__strTail x

83

84-- we need the 'believe_me' because the operations are primitives

libs/prelude/Prelude/Vect.idr+20−19

@@ -37,8 +37,8 @@ length (x::xs) = 1 + length xs

37

38||| Show that the length function on vectors in fact calculates the length

39private lengthCorrect : (n : Nat) -> (xs : Vect n a) -> length xs = n

40−lengthCorrect Z [] = refl

40+lengthCorrect Z [] = Refl

41−lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in refl

41+lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl

42

43--------------------------------------------------------------------------------

44-- Indexing into vectors

@@ -64,35 +64,36 @@ init (x::y::ys) = x :: init (y::ys)

64

65||| Extract a particular element from a vector

66index : Fin n -> Vect n a -> a

67−index fZ (x::xs) = x

67+index FZ (x::xs) = x

68−index (fS k) (x::xs) = index k xs

68+index (FS k) (x::xs) = index k xs

69−index fZ [] impossible

69+index FZ [] impossible

70+

70

71

71||| Insert an element at a particular index

72||| Insert an element at a particular index

72insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a

73insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a

73−insertAt fZ y xs = y :: xs

74+insertAt FZ y xs = y :: xs

74−insertAt (fS k) y (x::xs) = x :: insertAt k y xs

75+insertAt (FS k) y (x::xs) = x :: insertAt k y xs

75−insertAt (fS k) y [] = absurd k

76+insertAt (FS k) y [] = absurd k

76

77

77||| Construct a new vector consisting of all but the indicated element

78||| Construct a new vector consisting of all but the indicated element

78deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a

79deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a

79−deleteAt fZ (x::xs) = xs

80+deleteAt FZ (x::xs) = xs

80−deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs

81+deleteAt {n = S m} (FS k) (x::xs) = x :: deleteAt k xs

81−deleteAt {n = Z} (fS k) (x::xs) = absurd k

82+deleteAt {n = Z} (FS k) (x::xs) = absurd k

82deleteAt _ [] impossible

83deleteAt _ [] impossible

83

84

84||| Replace an element at a particlar index with another

85||| Replace an element at a particlar index with another

85replaceAt : Fin n -> t -> Vect n t -> Vect n t

86replaceAt : Fin n -> t -> Vect n t -> Vect n t

86−replaceAt fZ y (x::xs) = y :: xs

87+replaceAt FZ y (x::xs) = y :: xs

87−replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs

88+replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs

88

89

89||| Replace the element at a particular index with the result of applying a function to it

90||| Replace the element at a particular index with the result of applying a function to it

90||| @ i the index to replace at

91||| @ i the index to replace at

91||| @ f the update function

92||| @ f the update function

92||| @ xs the vector to replace in

93||| @ xs the vector to replace in

93updateAt : (i : Fin n) -> (f : t -> t) -> (xs : Vect n t) -> Vect n t

94updateAt : (i : Fin n) -> (f : t -> t) -> (xs : Vect n t) -> Vect n t

94−updateAt fZ f (x::xs) = f x :: xs

95+updateAt FZ f (x::xs) = f x :: xs

95−updateAt (fS k) f (x::xs) = x :: updateAt k f xs

96+updateAt (FS k) f (x::xs) = x :: updateAt k f xs

96

97

97--------------------------------------------------------------------------------

98--------------------------------------------------------------------------------

98-- Subvectors

99-- Subvectors

@@ -460,7 +461,7 @@ diag ((x::xs)::xss) = x :: diag (map tail xss)

460

461

461range : Vect n (Fin n)

462range : Vect n (Fin n)

462range {n=Z} = []

463range {n=Z} = []

463−range {n=S _} = fZ :: map fS range

464+range {n=S _} = FZ :: map FS range

464

465

465||| Transpose a Vect of Vects, turning rows into columns and vice versa.

466||| Transpose a Vect of Vects, turning rows into columns and vice versa.

466|||

467|||

@@ -474,15 +475,15 @@ transpose (x :: xs) = zipWith (::) x (transpose xs)

474--------------------------------------------------------------------------------

475--------------------------------------------------------------------------------

475

476

476vectConsCong : (x : a) -> (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> (x :: xs = x :: ys)

477vectConsCong : (x : a) -> (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> (x :: xs = x :: ys)

477−vectConsCong x xs xs refl = refl

478+vectConsCong x xs xs Refl = Refl

478

479

479vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs

480vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs

480−vectNilRightNeutral [] = refl

481+vectNilRightNeutral [] = Refl

481vectNilRightNeutral (x :: xs) =

482vectNilRightNeutral (x :: xs) =

482 vectConsCong _ _ _ (vectNilRightNeutral xs)

483 vectConsCong _ _ _ (vectNilRightNeutral xs)

483

484

484vectAppendAssociative : (x : Vect xLen a) -> (y : Vect yLen a) -> (z : Vect zLen a) -> x ++ (y ++ z) = (x ++ y) ++ z

485vectAppendAssociative : (x : Vect xLen a) -> (y : Vect yLen a) -> (z : Vect zLen a) -> x ++ (y ++ z) = (x ++ y) ++ z

485−vectAppendAssociative [] y z = refl

486+vectAppendAssociative [] y z = Refl

486vectAppendAssociative (x :: xs) ys zs =

487vectAppendAssociative (x :: xs) ys zs =

487 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)

488 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)

488

489

samples/binary.idr+1−1

@@ -19,7 +19,7 @@ instance Show (Binary w k) where

19 show (bin # bit) = show bin ++ show bit

20

21pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))

22−term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, refl)))

22+term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, Refl)))

23

24addBit : Bit x -> Bit y -> Bit c ->

25 (bx ** (by ** (Bit bx, Bit by, c + x + y = by + 2 * bx)))

samples/interp-alt.idr+13−13

@@ -14,12 +14,12 @@ using (G : Vect n Ty)

14 (::) : interpTy a -> Env G -> Env (a :: G)

15

16-- data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where

17−-- stop : HasType fZ (t :: G) t

17+-- stop : HasType FZ (t :: G) t

18−-- pop : HasType k G t -> HasType (fS k) (u :: G) t

18+-- pop : HasType k G t -> HasType (FS k) (u :: G) t

19

20 lookup : (i:Fin n) -> Env G -> interpTy (index i G)

21− lookup fZ (x :: xs) = x

21+ lookup FZ (x :: xs) = x

22− lookup (fS i) (x :: xs) = lookup i xs

22+ lookup (FS i) (x :: xs) = lookup i xs

23

24 data Expr : Vect n Ty -> Ty -> Type where

25 Var : (i : Fin n) -> Expr G (index i G)

@@ -41,32 +41,32 @@ using (G : Vect n Ty)

41 interp env (Bind v f) = interp env (f (interp env v))

42

43 eId : Expr G (TyFun TyInt TyInt)

44− eId = Lam (Var fZ)

44+ eId = Lam (Var FZ)

45

46 eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))

47− eTEST = Lam (Lam (Var (fS fZ)))

47+ eTEST = Lam (Lam (Var (FS FZ)))

48

49 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))

50− eAdd = Lam (Lam (Op prim__addInt (Var fZ) (Var (fS fZ))))

50+ eAdd = Lam (Lam (Op prim__addInt (Var FZ) (Var (FS FZ))))

51

52-- eDouble : Expr G (TyFun TyInt TyInt)

53−-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fZ) (Var (fS fZ))))) (Var fZ)) (Var fZ))

53+-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var FZ) (Var (FS FZ))))) (Var FZ)) (Var FZ))

54

55 eDouble : Expr G (TyFun TyInt TyInt)

56− eDouble = Lam (App (App eAdd (Var fZ)) (Var fZ))

56+ eDouble = Lam (App (App eAdd (Var FZ)) (Var FZ))

57

58 app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

59 app = \f, a => App f a

60

61 eFac : Expr G (TyFun TyInt TyInt)

62− eFac = Lam (If (Op (==) (Var fZ) (Val 0))

62+ eFac = Lam (If (Op (==) (Var FZ) (Val 0))

63− (Val 1) (Op (*) (app eFac (Op (-) (Var fZ) (Val 1))) (Var fZ)))

63+ (Val 1) (Op (*) (app eFac (Op (-) (Var FZ) (Val 1))) (Var FZ)))

64

65 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2

66

67 eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt))

68− eProg = Lam (Lam (Bind (App eDouble (Var (fS fZ)))

68+ eProg = Lam (Lam (Bind (App eDouble (Var (FS FZ)))

69− (\x => Bind (App eDouble (Var fZ))

69+ (\x => Bind (App eDouble (Var FZ))

70 (\y => Bind (App eDouble (Val x))

71 (\z => App (App eAdd (Val y)) (Val z))))))

72

samples/interp.idr+2−2

@@ -14,8 +14,8 @@ using (G : Vect n Ty)

14 (::) : interpTy a -> Env G -> Env (a :: G)

15

16 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where

17− stop : HasType fZ (t :: G) t

17+ stop : HasType FZ (t :: G) t

18− pop : HasType k G t -> HasType (fS k) (u :: G) t

18+ pop : HasType k G t -> HasType (FS k) (u :: G) t

19

20 lookup : HasType i G t -> Env G -> interpTy t

21 lookup stop (x :: xs) = x

samples/reflection.idr+2−2

@@ -32,13 +32,13 @@ envList = ?envListPrf

32

33||| Reflected raw rep. for the type (TTName, TT)

34tupleType : Raw

35−tupleType = RApp (RApp (Var (MN 0 "__Pair"))

35+tupleType = RApp (RApp (Var (UN "Pair"))

36 (Var (NS (UN "TTName") ["Reflection", "Language"])))

37 (Var (NS (UN "TT") ["Reflection", "Language"]))

38

39||| Reflected raw rep for the type List (TTName, TT)

40mkTuple : Raw

41−mkTuple = RApp (RApp (Var (MN 0 "__MkPair"))

41+mkTuple = RApp (RApp (Var (UN "MkPair"))

42 (Var (NS (UN "TTName") ["Reflection", "Language"])))

43 (Var (NS (UN "TT") ["Reflection", "Language"]))

44

src/Idris/AbsSyntaxTree.hs+9−39

@@ -1063,18 +1063,12 @@ getInferType (App (App _ ty) _) = ty

1063

1064

1065

1066−-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class

1066+-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign

1067

1068−primNames = [unitTy, unitCon,

1069− falseTy, pairTy, pairCon,

1070− eqTy, eqCon, inferTy, inferCon]

1068+primNames = [falseTy, eqTy, eqCon, inferTy, inferCon]

1071

1069

1072−unitDoc = parseDocstring . T.pack $ "The canonical single-element type, also known as the trivially true proposition."

1073−unitTy = sMN 0 "__Unit"

1070+unitTy = sUN "Unit"

1074−unitCon = sMN 0 "__II"

1071+unitCon = sUN "MkUnit"

1075−unitDecl = PDatadecl unitTy PType

1076− [(parseDocstring . T.pack $ "The trivial constructor for `()`. ", [], unitCon, PRef bi unitTy, bi, [])]

1077−unitOpts = [DefaultEliminator]

1078

1072

1079falseDoc = parseDocstring . T.pack $

1073falseDoc = parseDocstring . T.pack $

1080 "The empty type, also known as the trivially false proposition." ++

1074 "The empty type, also known as the trivially false proposition." ++

@@ -1085,28 +1079,11 @@ falseTy = sMN 0 "__False"

1085falseDecl = PDatadecl falseTy PType []

1079falseDecl = PDatadecl falseTy PType []

1086falseOpts = []

1080falseOpts = []

1087

1081

1088−pairDoc = parseDocstring . T.pack $ "The non-dependent pair type, also known as conjunction."

1089−pairTy = sMN 0 "__Pair"

1082+pairTy = sUN "Pair"

1090−pairCon = sMN 0 "__MkPair"

1083+pairCon = sUN "MkPair"

1091−pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

1092− [(pairConDoc, pairConParamDoc,

1093− pairCon, PPi impl (n "A") PType (

1094− PPi impl (n "B") PType (

1095− PPi expl (n "a") (PRef bi (n "A")) (

1096− PPi expl (n "b") (PRef bi (n "B"))

1097− (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

1098− pexp (PRef bi (n "B"))])))), bi, [])]

1099− where n a = sMN 0 a

1100− pairConDoc = parseDocstring . T.pack $ "A pair of elements"

1101− pairConParamDoc = [(n "a", parseDocstring . T.pack $ "the left element of the pair"),

1102− (n "b", parseDocstring . T.pack $ "the right element of the pair")]

1103−pairOpts = []

1104−pairParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left elements in the pair"),

1105− (n "B", parseDocstring . T.pack $ "the type of the left elements in the pair")]

1106− where n a = sMN 0 a

1107

1084

1108eqTy = sUN "="

1085eqTy = sUN "="

1109−eqCon = sUN "refl"

1086+eqCon = sUN "Refl"

1110eqDoc = parseDocstring . T.pack $

1087eqDoc = parseDocstring . T.pack $

1111 "The propositional equality type. A proof that `x` = `y`." ++

1088 "The propositional equality type. A proof that `x` = `y`." ++

1112 "\n\n" ++

1089 "\n\n" ++

@@ -1143,16 +1120,9 @@ eqParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left side of th

1143

1120

1144eqOpts = []

1121eqOpts = []

1145

1122

1146−elimName = sUN "__Elim"

1147−elimMethElimTy = sUN "__elimTy"

1148−elimMethElim = sUN "elim"

1149−elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)] []

1150− [PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElimTy PType,

1151− PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1152−

1153-- Defined in builtins.idr

1123-- Defined in builtins.idr

1154sigmaTy = sUN "Sigma"

1124sigmaTy = sUN "Sigma"

1155−existsCon = sUN "Sg_intro"

1125+existsCon = sUN "MkSigma"

1156

1126

1157piBind :: [(Name, PTerm)] -> PTerm -> PTerm

1127piBind :: [(Name, PTerm)] -> PTerm -> PTerm

1158piBind = piBindp expl

1128piBind = piBindp expl

@@ -1338,7 +1308,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1338

1308

1339 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r

1309 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r

1340 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm

1310 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm

1341− prettySe p bnd (PRefl _ _) = annName eqCon $ text "refl"

1311+ prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"

1342 prettySe p bnd (PResolveTC _) = text "resolvetc"

1312 prettySe p bnd (PResolveTC _) = text "resolvetc"

1343 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"

1313 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"

1344 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

1314 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

src/Idris/Apropos.hs+1−1

@@ -41,7 +41,7 @@ instance Apropos Name where

41 | n == falseTy && str == T.pack "_|_" = True

42 | (n == pairTy || n == pairCon) && str == T.pack "," = True

43 | n == eqTy && str == T.pack "=" = True

44− | n == eqCon && (T.toLower str) == T.pack "refl" = True

44+ | n == eqCon && (T.toLower str) == T.pack "Refl" = True

45 | (n == sigmaTy || n == existsCon) && str == T.pack "**" = True

46 isApropos _ _ = False -- we don't care about case blocks, MNs, etc

47

src/Idris/ElabDecls.hs+4−5

@@ -76,12 +76,11 @@ elabPrims :: Idris ()

76elabPrims = do mapM_ (elabDecl' EAll recinfo)

77 (map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)

78 (zip4

79− [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

79+ [inferOpts, falseOpts, eqOpts]

80− [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]

80+ [inferDecl, falseDecl, eqDecl]

81− [emptyDocstring, unitDoc, falseDoc, pairDoc, eqDoc]

81+ [emptyDocstring, falseDoc, eqDoc]

82− [[], [], [], pairParamDoc, eqParamDoc]))

82+ [[], [], eqParamDoc]))

83 addNameHint eqTy (sUN "prf")

84− elabDecl' EAll recinfo elimDecl

85 mapM_ elabPrim primitives

84 mapM_ elabPrim primitives

86 -- Special case prim__believe_me because it doesn't work on just constants

85 -- Special case prim__believe_me because it doesn't work on just constants

87 elabBelieveMe

86 elabBelieveMe

src/Idris/ElabTerm.hs+10−6

@@ -245,8 +245,12 @@ elab ist info emode opts fn tm

245-- = lift $ tfail (Msg "Typecase is not allowed")

246 elab' ina (PConstant c) = do apply (RConstant c) []; solve

247 elab' ina (PQuote r) = do fill r; solve

248− elab' ina (PTrue fc _) = try (elab' ina (PRef fc unitCon))

248+ elab' ina (PTrue fc _) =

249+ do hnf_compute

250+ g <- goal

251+ case g of

249− (elab' ina (PRef fc unitTy))

252+ TType _ -> elab' ina (PRef fc unitTy)

253+ _ -> elab' ina (PRef fc unitCon)

250 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)

254 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)

251 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

255 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

252 = do g <- goal; resolveTC False 5 g fn ist

256 = do g <- goal; resolveTC False 5 g fn ist

@@ -283,11 +287,11 @@ elab ist info emode opts fn tm

283 = do hnf_compute

287 = do hnf_compute

284 g <- goal

288 g <- goal

285 case g of

289 case g of

286− TType _ -> elabE (True, a,inty, qq) (PApp fc (PRef fc pairTy)

290+ TType _ -> elab' ina (PApp fc (PRef fc pairTy)

287 [pexp l,pexp r])

291 [pexp l,pexp r])

288− _ -> elabE (True, a, inty, qq) (PApp fc (PRef fc pairCon)

292+ _ -> elab' ina (PApp fc (PRef fc pairCon)

289− [pimp (sMN 0 "A") Placeholder True,

293+ [pimp (sUN "A") Placeholder False,

290− pimp (sMN 0 "B") Placeholder True,

294+ pimp (sUN "B") Placeholder False,

291 pexp l, pexp r])

295 pexp l, pexp r])

292 elab' ina (PDPair fc p l@(PRef _ n) t r)

296 elab' ina (PDPair fc p l@(PRef _ n) t r)

293 = case t of

297 = case t of

src/Idris/Erasure.hs+3−3

@@ -201,7 +201,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

201

202 -- these have been discovered as builtins but are not listed

203 -- among Idris.Primitives.primitives

204− , mn "__MkPair" [2,3]

204+ --, mn "__MkPair" [2,3]

205 , it "prim_fork" [0]

206 , it "unsafePerformPrimIO" [1]

207

@@ -348,8 +348,8 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

348 -- assumed to be a global reference

349 | otherwise = M.singleton cd (M.singleton (n, Result) S.empty)

350 where

351− specialMNs = map (sMN 0 . ("__" ++)) $ words "Unit True False II"

351+ specialMNs = [falseTy]

352−

352+

353 -- dependencies of de bruijn variables are described in `bs'

354 getDepsTerm vs bs cd (V i) = snd (bs !! i) cd

355

src/Idris/ParseExpr.hs+2−2

@@ -278,7 +278,7 @@ SimpleExpr ::=

278 {- External (User-defined) Simple Expression -}

279 | '?' Name

280 | % 'instance'

281− | 'refl' ('{' Expr '}')?

281+ | 'Refl' ('{' Expr '}')?

282 | ProofExpr

283 | TacticsExpr

284 | FnName

@@ -300,7 +300,7 @@ simpleExpr syn =

300 try (simpleExternalExpr syn)

301 <|> do x <- try (lchar '?' *> name); return (PMetavar x)

302 <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)

303− <|> do reserved "refl"; fc <- getFC;

303+ <|> do reserved "Refl"; fc <- getFC;

304 tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';

305 return t)

306 return (PRefl fc tm)

test/basic001/basic001a.idr+1−1

@@ -13,7 +13,7 @@ rle [] = REnd

13rle (x :: xs) with (rle xs)

14 rle (x :: []) | REnd = RChar 0 x REnd

15 rle (x :: (c :: (replicate n c ++ ys))) | (RChar n c rs) with (decEq x c)

16− rle (x :: (x :: (replicate n x ++ ys))) | (RChar n x rs) | (Yes refl)

16+ rle (x :: (x :: (replicate n x ++ ys))) | (RChar n x rs) | (Yes Refl)

17 = RChar (S n) x rs

18 rle (x :: (c :: (replicate n c ++ ys))) | (RChar n c rs) | (No f)

19 = RChar 0 x (RChar n c rs)

test/basic001/reg005.idr+2−2

@@ -16,7 +16,7 @@ data RLE : Vect n Char -> Type where

16 -> RLE (rep (S n) x ++ xs)

17

18eq : (x : Char) -> (y : Char) -> Maybe (x = y)

19−eq x y = if x == y then Just (believe_me (refl {x})) else Nothing

19+eq x y = if x == y then Just (believe_me (Refl {x})) else Nothing

20

21------------

22

@@ -25,7 +25,7 @@ rle [] = REnd

25rle (x :: xs) with (rle xs)

26 rle (x :: Vect.Nil) | REnd = RChar Z x REnd

27 rle (x :: rep (S n) yvar ++ ys) | RChar n yvar rs with (eq x yvar)

28− rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just refl

28+ rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just Refl

29 = RChar (S n) x rs

30 rle (x :: rep (S n) y ++ ys) | RChar n y rs | Nothing

31 = RChar Z x (RChar n y rs)

test/basic005/test019.lidr+6−6

@@ -1,16 +1,16 @@

1> module Main

2

3−> ifTrue : so True -> Nat

3+> ifTrue : So True -> Nat

4−> ifTrue oh = S Z

4+> ifTrue Oh = S Z

5

6−> ifFalse : so False -> Nat

6+> ifFalse : So False -> Nat

7−> ifFalse oh impossible

7+> ifFalse Oh impossible

8

9−> test : (f : Nat -> Bool) -> (n : Nat) -> so (f n) -> Nat

9+> test : (f : Nat -> Bool) -> (n : Nat) -> So (f n) -> Nat

10> test f n x with (f n)

11> | True = ifTrue x

12> | False = ifFalse x

13

14> main : IO ()

15−> main = print (test ((S 4) ==) 5 oh)

15+> main = print (test ((S 4) ==) 5 Oh)

16

test/basic009/Faulty.idr+1−1

@@ -4,4 +4,4 @@ import A

4import B.C

5

6fault : num = Z

7−fault = refl

7+fault = Refl

test/basic009/Main.idr+4−4

@@ -4,13 +4,13 @@ import A as X

4import B.C as Y

5

6checkX : X.num = Z

7−checkX = refl

7+checkX = Refl

8

9checkY : Y.num = S Z

10−checkY = refl

10+checkY = Refl

11

12checkAX : X.num = A.num

13−checkAX = refl

13+checkAX = Refl

14

15checkBY : Y.num = B.C.num

16−checkBY = refl

16+checkBY = Refl

test/basic010/Main.idr+2−2

@@ -20,7 +20,7 @@ eq_refl {n = S n} = eqS eq_refl

20-- Here, the proof is very expensive to compute.

21-- We add a recursive argument to prevent Idris from inlining the function.

22f : (r, n : Nat) -> Subset Nat (\k => qib n `equals` qib k)

23−f Z n = element n eq_refl

23+f Z n = Element n eq_refl

24f (S r) n = f r n

25

26-- A (contrived) relation, just to have something to show.

@@ -30,7 +30,7 @@ data represents : Nat -> Nat -> Type where

30-- Here, the witness is very expensive to compute.

31-- We add a recursive argument to prevent Idris from inlining the function.

32g : (r, n : Nat) -> Exists (\k : Nat => k `represents` n)

33−g Z n = evidence (qib n) (axiom n)

33+g Z n = Evidence (qib n) (axiom n)

34g (S r) n = g r n

35

36fmt : qib n `represents` n -> String

test/dsl001/test001.idr+3−3

@@ -14,8 +14,8 @@ using (G : Vect n Ty)

14 (::) : interpTy a -> Env G -> Env (a :: G)

15

16 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where

17− stop : HasType fZ (t :: G) t

17+ stop : HasType FZ (t :: G) t

18− pop : HasType k G t -> HasType (fS k) (u :: G) t

18+ pop : HasType k G t -> HasType (FS k) (u :: G) t

19

20 lookup : HasType i G t -> Env G -> interpTy t

21 lookup stop (x :: xs) = x

@@ -58,7 +58,7 @@ using (G : Vect n Ty)

58 eAdd = expr (\x, y => Op (+) x y)

59

60-- eDouble : Expr G (TyFun TyInt TyInt)

61−-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fZ) (Var (fS fZ))))) (Var fZ)) (Var fZ))

61+-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var FZ) (Var (FS FZ))))) (Var FZ)) (Var FZ))

62

63 eDouble : Expr G (TyFun TyInt TyInt)

64 eDouble = expr (\x => App (App eAdd x) (Var stop))

test/dsl002/Resimp.idr+2−2

@@ -46,8 +46,8 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)

46 interpTy (a :-> b) = a -> interpTy b

47

48 data HasType : Vect n Ty -> Fin n -> Ty -> Type where

49− stop : HasType (a :: gam) fZ a

49+ stop : HasType (a :: gam) FZ a

50− pop : HasType gam i b -> HasType (a :: gam) (fS i) b

50+ pop : HasType gam i b -> HasType (a :: gam) (FS i) b

51

52 data Env : Vect n Ty -> Type where

53 Nil : Env Nil

test/dsl003/DSLPi.idr+5−5

@@ -6,7 +6,7 @@ dsl simple_type

6 pi = ARR

7

8test1 : simple_type (BOOL -> INT -> UNIT) = BOOL `ARR` (INT `ARR` UNIT)

9−test1 = refl

9+test1 = Refl

10

11using (vars : Vect n Ty)

12 infix 2 ===

@@ -25,14 +25,14 @@ using (vars : Vect n Ty)

25dsl specs

26 pi = ForAll

27 variable = Var

28− index_first = fZ

28+ index_first = FZ

29− index_next = fS

29+ index_next = FS

30

31test2 : Spec []

32test2 = specs ((x, y : INT) -> x === y)

33

34test3 : Spec []

35−test3 = ForAll INT . ForAll INT . ItHolds $ Var (fS fZ) === Var fZ

35+test3 = ForAll INT . ForAll INT . ItHolds $ Var (FS FZ) === Var FZ

36

37test4 : test2 = test3

38−test4 = refl

38+test4 = Refl

test/dsl003/expected+2−2

@@ -1,2 +1,2 @@

1−ForAll INT (ForAll INT (ItHolds (Var (fS fZ) === Var fZ))) : Spec []

1+ForAll INT (ForAll INT (ItHolds (Var (FS FZ) === Var FZ))) : Spec []

2−refl : ARR BOOL (ARR INT UNIT) = ARR BOOL (ARR INT UNIT)

2+Refl : ARR BOOL (ARR INT UNIT) = ARR BOOL (ARR INT UNIT)

test/effects002/test025.idr+6−6

@@ -16,14 +16,14 @@ sub1 xs = map (prim__truncInt_B8 . (\ x => x - 1) . prim__zextB8_Int) xs

16

17testMemory : MemoryIO () () (Vect 4 Int)

18testMemory = do Src :- allocate 5

19− Src :- poke 0 inpVect oh

19+ Src :- poke 0 inpVect Oh

20 Dst :- allocate 5

21− Dst :- initialize (prim__truncInt_B8 1) 2 oh

21+ Dst :- initialize (prim__truncInt_B8 1) 2 Oh

22− move 2 2 3 oh oh

22+ move 2 2 3 Oh Oh

23 Src :- free

24− end <- Dst :- peek 4 (S Z) oh

24+ end <- Dst :- peek 4 (S Z) Oh

25− Dst :- poke 4 (sub1 end) oh

25+ Dst :- poke 4 (sub1 end) Oh

26− res <- Dst :- peek 1 (S(S(S(S Z)))) oh

26+ res <- Dst :- peek 1 (S(S(S(S Z)))) Oh

27 Dst :- free

28 return (map (prim__zextB8_Int) res)

29

test/error004/FunErrTest.idr+3−3

@@ -11,9 +11,9 @@ cadr : (xs : List a)

11 -> {auto cons1 : isCons xs = True}

12 -> {auto cons2 : isCons (tail xs) = True}

13 -> a

14−cadr (x :: (y :: _)) {cons1=refl} {cons2=refl} = y

14+cadr (x :: (y :: _)) {cons1=Refl} {cons2=Refl} = y

15−cadr (x :: []) {cons1=refl} {cons2=refl} impossible

15+cadr (x :: []) {cons1=Refl} {cons2=Refl} impossible

16−cadr [] {cons1=refl} {cons2=refl} impossible

16+cadr [] {cons1=Refl} {cons2=Refl} impossible

17

18extractList : TT -> Maybe TT

19extractList (App (App reflCon (App isCons lst)) _) = Just lst

test/ffi002/test023.idr+2−2

@@ -10,9 +10,9 @@ import Providers

10goodProvider : IO (Provider Type)

11goodProvider = return (Provide (the Type ()))

12

13−%provide (Unit : Type) with goodProvider

13+%provide (Unit' : Type) with goodProvider

14

15−foo : Unit

15+foo : Unit'

16foo = ()

17

18-- Always fail

test/interactive001/expected+1−1

@@ -7,7 +7,7 @@ isElem x (y :: xs) = ?isElem_rhs_3

7f x :: map f xs

8isElem2 x (y :: ys) with (_)

9 isElem2 x (y :: ys) | with_pat = ?isElem2_rhs

10− isElem3 x (x :: ys) | (Yes refl) = ?isElem3_rhs_3

10+ isElem3 x (x :: ys) | (Yes Refl) = ?isElem3_rhs_3

11

12 [] => ?bar_1

13 (x :: ys) => ?bar_2

test/io003/test018a.idr+5−5

@@ -4,17 +4,17 @@ import System.Concurrency.Process

4

5ping : ProcID String -> ProcID String -> Process String ()

6ping main proc

7− = do lift (usleep 1000)

7+ = do Lift (usleep 1000)

8 send proc "Hello!"

9− lift (putStrLn "Sent ping")

9+ Lift (putStrLn "Sent ping")

10 msg <- recv

11− lift (putStrLn ("Reply: " ++ show msg))

11+ Lift (putStrLn ("Reply: " ++ show msg))

12 send main "Done"

13

14pong : Process String ()

15−pong = do -- lift (putStrLn "Waiting for message")

15+pong = do -- Lift (putStrLn "Waiting for message")

16 (sender, m) <- recvWithSender

17− lift $ putStrLn ("Received " ++ m)

17+ Lift $ putStrLn ("Received " ++ m)

18 send sender ("Hello back!")

19

20mainProc : Process String ()

test/primitives003/test038.idr+5−5

@@ -2,7 +2,7 @@ module Main

2

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

4test i1 i2 with (decEq i1 i2)

5− test i1 i1 | Yes refl = True

5+ test i1 i1 | Yes Refl = True

6 test i1 i2 | No p = False

7

8main : IO ()

@@ -52,10 +52,10 @@ main = do

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))))

55+ putStrLn . show $ test (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))

56− (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))))

57+ putStrLn . show $ test (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))

58− (the (Fin (S (S (S (Z))))) (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))

test/proof001/test029.idr+2−2

@@ -5,13 +5,13 @@ plus_comm : (n : Nat) -> (m : Nat) -> (n + m = m + n)

5-- Base case

6(Z + m = m + Z) <== plus_comm =

7 rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>

8− (Z + m = m) in refl

8+ (Z + m = m) in Refl

9

10-- Step case

11(S k + m = m + S k) <== plus_comm =

12 rewrite ((k + m = m + k) <== plus_comm) in

13 rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in

14− refl

14+ Refl

15-- QED

16

17append : Vect n a -> Vect m a -> Vect (m + n) a

test/proof002/Reflect.idr+9−9

@@ -36,8 +36,8 @@ using (xs : List a, ys : List a, G : List (List a))

36-- list appends

37

38 expr_r : Expr G xs -> (xs' ** (RExpr G xs', xs = xs'))

39− expr_r ENil = (_ ** (RNil, refl))

39+ expr_r ENil = (_ ** (RNil, Refl))

40− expr_r (Var i) = (_ ** (RApp RNil i, refl))

40+ expr_r (Var i) = (_ ** (RApp RNil i, Refl))

41 expr_r (App ex ey) = let (xl ** (xr, xprf)) = expr_r ex in

42 let (yl ** (yr, yprf)) = expr_r ey in

43 appRExpr _ _ xr yr xprf yprf

@@ -47,7 +47,7 @@ using (xs : List a, ys : List a, G : List (List a))

47 RExpr G xs -> RExpr G ys -> (xs' = xs) -> (ys' = ys) ->

48 (ws' ** (RExpr G ws', xs' ++ ys' = ws'))

49 appRExpr x' y' rxs (RApp e i) xprf yprf

50− = let (xs ** (rec, prf)) = appRExpr _ _ rxs e refl refl in

50+ = let (xs ** (rec, prf)) = appRExpr _ _ rxs e Refl Refl in

51 (_ ** (RApp rec i, ?appRExpr1))

52 appRExpr x' y' rxs RNil xprf yprf = (_ ** (rxs, ?appRExpr2))

53

@@ -68,12 +68,12 @@ using (xs : List a, ys : List a, G : List (List a))

68 eqExpr : (e : Expr G xs) -> (e' : Expr G ys) ->

69 Maybe (e = e')

70 eqExpr (App x y) (App x' y') with (eqExpr x x', eqExpr y y')

71− eqExpr (App x y) (App x y) | (Just refl, Just refl) = Just refl

71+ eqExpr (App x y) (App x y) | (Just Refl, Just Refl) = Just Refl

72 eqExpr (App x y) (App x' y') | _ = Nothing

73 eqExpr (Var i) (Var j) with (prim__syntactic_eq _ _ i j)

74− eqExpr (Var i) (Var i) | (Just refl) = Just refl

74+ eqExpr (Var i) (Var i) | (Just Refl) = Just Refl

75 eqExpr (Var i) (Var j) | _ = Nothing

76− eqExpr ENil ENil = Just refl

76+ eqExpr ENil ENil = Just Refl

77 eqExpr _ _ = Nothing

78

79-- Given a couple of reflected expressions, try to produce a proof that

@@ -83,7 +83,7 @@ using (xs : List a, ys : List a, G : List (List a))

83 Expr G ln -> Expr G rn ->

84 (xs = ln) -> (ys = rn) -> Maybe (xs = ys)

85 buildProof e e' lp rp with (eqExpr e e')

86− buildProof e e lp rp | Just refl = ?bp1

86+ buildProof e e lp rp | Just Refl = ?bp1

87 buildProof e e' lp rp | Nothing = Nothing

88

89 testEq : Expr G xs -> Expr G ys -> Maybe (xs = ys)

@@ -108,7 +108,7 @@ using (xs : List a, ys : List a, G : List (List a))

108 isElem : (x : a) -> (xs : List a) -> Maybe (Elem x xs)

109 isElem x [] = Nothing

110 isElem x (y :: ys) with (prim__syntactic_eq _ _ x y)

111− isElem x (x :: ys) | Just refl = [| Stop |]

111+ isElem x (x :: ys) | Just Refl = [| Stop |]

112 isElem x (y :: ys) | Nothing = [| Pop (isElem x ys) |]

113

114 weakenElem : (G' : List a) -> Elem x xs -> Elem x (G' ++ xs)

@@ -126,7 +126,7 @@ using (xs : List a, ys : List a, G : List (List a))

126-- %reflection means a function runs on syntax, rather than on constructors.

127-- So, 'reflectList' builds a reflected List expression as defined above.

128

129−-- It also converts (x :: xs) into a reflected [x] ++ xs so that the above

129+-- It also converts (x :: xs) into a reflected [x] ++ xs So that the above

130-- reduction will work the right way.

131

132%reflection

test/proof003/test015.idr+1−1

@@ -45,7 +45,7 @@ testBin : Maybe (Binary 8 42)

45testBin = natToBin _ _

46

47pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))

48−term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, refl)))

48+term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, Refl)))

49

50addBit : Bit x -> Bit y -> Bit c ->

51 (bX ** (bY ** (Bit bX, Bit bY, c + x + y = bY + 2 * bX)))

test/quasiquote001/expected+3−3

@@ -1,5 +1,5 @@

1−(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 10)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 10))))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 10)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 10))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 10))))))

1+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 9 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 9 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 9 0) (UN Unit) (TType (UVar -1))))))

2--------------

3−(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 190))) (TType (UVar 192))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 194))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 196)))))

3+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 50))) (TType (UVar 52))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 54))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (P (TCon 9 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 9 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 56)))))

4--------------

5−(App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (TType (UVar 190))) (TType (UVar 190)))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (TType (UVar 190))) (TType (UVar 190))))

5+(App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (TType (UVar 50))) (TType (UVar 50)))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (TType (UVar 50))) (TType (UVar 50))))

test/quasiquote003/NoInfer.idr+2−2

@@ -4,7 +4,7 @@ import Language.Reflection

4import Language.Reflection.Utils

5

6zzz2 : TT

7−zzz2 = `(fZ : Fin 3)

7+zzz2 = `(FZ : Fin 3)

8

9zzz : TT

10−zzz = `(fZ)

10+zzz = `(FZ)

test/quasiquote004/Quasiquote004.idr+1−1

@@ -24,7 +24,7 @@ data Fizzy : Nat -> Type where

24-- Fizzy is a correct specification of divisibility by 3 - that is, if n is

25-- fizzy then there exists some k such that n = 3*k.

26fizzyCorrect : (n : Nat) -> Fizzy n -> (k : Nat ** n = 3 * k)

27−fizzyCorrect Z ZeroFizzy = (Z ** refl)

27+fizzyCorrect Z ZeroFizzy = (Z ** Refl)

28fizzyCorrect (S (S (S k))) (Fizz x) =

29 let (k' ** ih) = fizzyCorrect k x

30 in (S k' ** ?fizzyIsAOK)

test/reg002/reg002.idr+2−2

@@ -17,10 +17,10 @@ S_Co_not_Inf : Main.S (Co n) = Infinity -> _|_

17S_Co_not_Inf = believe_me

18

19S_inj : (n : CoNat) -> (m : CoNat) -> Main.S n = Main.S m -> n = m

20−S_inj (Co n) (Co _) refl = refl

20+S_inj (Co n) (Co _) Refl = Refl

21S_inj (Co n) Infinity p = FalseElim (S_Co_not_Inf p)

22S_inj Infinity (Co m) p = FalseElim (S_Co_not_Inf (sym p))

23−S_inj Infinity Infinity refl = refl

23+S_inj Infinity Infinity Refl = Refl

24

25swap : {n : Nat} -> Vect n a -> Vect n a

26swap Nil = Nil

test/reg006/reg006.idr+3−3

@@ -8,9 +8,9 @@ data RBTree : Type -> Type -> Nat -> Colour -> Type where

8 BlackBranch : k -> v -> RBTree k v n x -> RBTree k v n y -> RBTree k v (S n) Black

9

10toBlack : RBTree k v n c -> (m ** (RBTree k v m Black, Either (m = n) (m = (S n))))

11−toBlack (RedBranch k v l r) = (_ ** (BlackBranch k v l r, Right refl))

11+toBlack (RedBranch k v l r) = (_ ** (BlackBranch k v l r, Right Refl))

12−toBlack Leaf = (_ ** (Leaf, Left refl))

12+toBlack Leaf = (_ ** (Leaf, Left Refl))

13−toBlack (BlackBranch k v l r) = (_ ** (BlackBranch k v l r, Left refl))

13+toBlack (BlackBranch k v l r) = (_ ** (BlackBranch k v l r, Left Refl))

14

15total

16lookup : Ord k => k -> RBTree k v n Black -> Maybe v

test/reg007/reg007.lidr+1−1

@@ -3,7 +3,7 @@

3> import A

4

5> isSame : A.n = A.lala

6−> isSame = refl

6+> isSame = Refl

7

8> A.n = Z -- This is where it's at!

9> A.lala = S Z

test/reg009/reg009.lidr+6−6

@@ -4,15 +4,15 @@

4

5> filterTagP : (p : alpha -> Bool) ->

6> (as : Vect n alpha) ->

7−> so (isAnyBy p (n ** as)) ->

7+> So (isAnyBy p (n ** as)) ->

8−> (m : Nat ** (Vect m (a : alpha ** so (p a)), so (m > Z)))

8+> (m : Nat ** (Vect m (a : alpha ** So (p a)), So (m > Z)))

9> filterTagP {n = S m} p (a :: as) q with (p a)

10> | True = (_

11> **

12−> ((a ** believe_me oh)

12+> ((a ** believe_me Oh)

13> ::

14−> (fst (getProof (filterTagP p as (believe_me oh)))),

14+> (fst (getProof (filterTagP p as (believe_me Oh)))),

15−> oh

15+> Oh

16> )

17> )

18−> | False = filterTagP p as (believe_me oh)

18+> | False = filterTagP p as (believe_me Oh)

test/reg012/reg012.lidr+11−11

@@ -1,21 +1,21 @@

1−> total soElim : (C : (b : Bool) -> so b -> Type) ->

1+> total soElim : (C : (b : Bool) -> So b -> Type) ->

2−> C True oh ->

2+> C True Oh ->

3−> (b : Bool) -> (s : so b) -> (C b s)

3+> (b : Bool) -> (s : So b) -> (C b s)

4−> soElim C coh .True .oh = coh

4+> soElim C coh .True .Oh = coh

5

6−> soFalseElim : so False -> a

6+> soFalseElim : So False -> a

7> soFalseElim x = FalseElim (soElim C () False x)

8> where

9−> C : (b : Bool) -> so b -> Type

9+> C : (b : Bool) -> So b -> Type

10> C True s = ()

11> C False s = _|_

12

13−> soTrue : so b -> b = True

13+> soTrue : So b -> b = True

14> soTrue {b = False} x = soFalseElim x

15−> soTrue {b = True} x = refl

15+> soTrue {b = True} x = Refl

16

17> class Eq alpha => ReflEqEq alpha where

18−> reflexive_eqeq : (a : alpha) -> so (a == a)

18+> reflexive_eqeq : (a : alpha) -> So (a == a)

19

20> modifyFun : (Eq alpha) =>

21> (alpha -> beta) ->

@@ -28,7 +28,7 @@

28> (ab : (alpha, beta)) ->

29> modifyFun f ab (fst ab) = snd ab

30> modifyFunLemma f (a,b) =

31−> rewrite soTrue (reflexive_eqeq a) in refl

31+> rewrite soTrue (reflexive_eqeq a) in Refl

32

33 replace {P = \ z => boolElim (a == a) b (f a) = boolElim z b (f a)}

34− (soTrue (reflexive_eqeq a)) refl

34+ (soTrue (reflexive_eqeq a)) Refl

test/reg017/reg017.idr+2−2

@@ -2,10 +2,10 @@ module Main

2

3foo : { t : Type } ->

4 (a : t) ->

5− { default tactics { refine refl; solve; } prfA : a = a } ->

5+ { default tactics { refine Refl; solve; } prfA : a = a } ->

6 (b : Nat) ->

7 (c : Nat) ->

8− { default tactics { refine refl; solve; } prfBC : b = c } ->

8+ { default tactics { refine Refl; solve; } prfBC : b = c } ->

9 Nat

10foo {t} a {prfA = p} b c {prfBC} = b

11

test/reg018/reg018d.idr+3−3

@@ -3,10 +3,10 @@ module Main

3total

4pull : Fin (S n) -> Vect (S n) a -> (a, Vect n a)

5pull {n=Z} _ (x :: xs) = (x, xs)

6−-- pull {n=S q} fZ (Vect.(::) {n=S _} x xs) = (x, xs)

6+-- pull {n=S q} FZ (Vect.(::) {n=S _} x xs) = (x, xs)

7−pull {n=S _} (fS n) (x :: xs) =

7+pull {n=S _} (FS n) (x :: xs) =

8 let (v, vs) = pull n xs in

9 (v, x::vs)

10

11main : IO ()

12−main = print (pull fZ [0, 1, 2])

12+main = print (pull FZ [0, 1, 2])

test/reg025/reg025.idr+7−7

@@ -21,22 +21,22 @@ Filled {n=n} = (\x => Not (Empty x))

21FullBoard : Board n -> Type

22FullBoard (MkBoard b) = All (All Filled) b

23

24−indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (fS i) (x::xs)

24+indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (FS i) (x::xs)

25−indexStep = refl

25+indexStep = Refl

26

27find : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a)

28 -> Either (All (\x => Not (P x)) xs) (y : a ** (P y, (i : Fin n ** y = index i xs)))

29find _ Nil = Left Nil

30find {P} d (x::xs) with (d x)

31− | Yes prf = Right (x ** (prf, (fZ ** refl)))

31+ | Yes prf = Right (x ** (prf, (FZ ** Refl)))

32 | No prf =

33 case find {P} d xs of

34 Right (y ** (prf', (i ** prf''))) =>

35− Right (y ** (prf', (fS i ** replace {P=(\x => y = x)} (indexStep {x=x}) prf'')))

35+ Right (y ** (prf', (FS i ** replace {P=(\x => y = x)} (indexStep {x=x}) prf'')))

36 Left prf' => Left (prf::prf')

37

38empty : (cell : Cell n) -> Dec (Empty cell)

39−empty Nothing = Yes refl

39+empty Nothing = Yes Refl

40empty (Just _) = No nothingNotJust

41

42findEmptyInRow : (xs : Vect n (Cell n)) -> Either (All Filled xs) (i : Fin n ** Empty (index i xs))

@@ -60,11 +60,11 @@ emptyCell (MkBoard rs) =

60 helper Nil = Left Nil

61 helper (r::rs) =

62 case findEmptyInRow r of

63− Right (ci ** pf3) => Right (fZ ** (ci ** pf3))

63+ Right (ci ** pf3) => Right (FZ ** (ci ** pf3))

64 Left prf =>

65 case helper rs of

66 Left prf' => Left (prf::prf')

67− Right (ri ** (ci ** pf4)) => Right (fS ri ** (ci ** pf4))

67+ Right (ri ** (ci ** pf4)) => Right (FS ri ** (ci ** pf4))

68

69

70main : IO ()

test/reg026/reg026.idr+1−1

@@ -1,7 +1,7 @@

1module Test

2

3X : Nat -> Type

4−X t = (c : Nat ** so (c < 5))

4+X t = (c : Nat ** So (c < 5))

5

6column : X t -> Nat

7column = getWitness

test/reg034/reg034.idr+2−2

@@ -3,8 +3,8 @@ import Prelude.List

3

4bar : (xs : List ()) -> (ys : List ()) ->

5 Prelude.List.length xs = Prelude.List.length ys -> xs = ys

6−bar xs xs refl = refl

6+bar xs xs Refl = Refl

7

8foo : (f : Nat -> Nat) -> (x : Nat) -> (y : Nat) -> f x = f y -> x = y

9−foo f x x refl = refl

9+foo f x x Refl = Refl

10

test/reg035/reg035.idr+2−2

@@ -2,10 +2,10 @@ elimId : (a : Type) ->

2 (a1 : a) ->

3 (a2 : a) ->

4 (m : (x : a) -> (y : a) -> x = y -> Type) ->

5− (f : (x : a) -> m x x refl) ->

5+ (f : (x : a) -> m x x Refl) ->

6 (id : a1 = a2) ->

7 m a1 a2 id

8−elimId _ x _ _ f refl = f x

8+elimId _ x _ _ f Refl = f x

9

10tran : (a : Type) -> (b : a) -> (c : a) -> (d : a) ->

11 (e : b = c) -> (f : c = d) -> b = d

test/reg035/reg035a.lidr+7−7

@@ -6,9 +6,9 @@

6> (q : beta -> Bool) ->

7> (a : alpha) ->

8> (b : beta) ->

9−> so (p a) ->

9+> So (p a) ->

10−> so (q b) ->

10+> So (q b) ->

11−> so (p a && q b)

11+> So (p a && q b)

12

13> hasNoDuplicates : (Eq alpha) => List alpha -> Bool

14> hasNoDuplicates as = as == nub as

@@ -33,7 +33,7 @@

33

34> postulate reflexive_Set_eqeq : (Eq a) =>

35> (as : Set a) ->

36−> so (as == as)

36+> So (as == as)

37

38> unwrap : Set a -> List a

39> unwrap (setify as) = as

@@ -53,14 +53,14 @@

53

54> partitionLemma0 : (Eq alpha) =>

55> (ass : Set (Set alpha)) ->

56−> so (arePairwiseDisjoint ass) ->

56+> So (arePairwiseDisjoint ass) ->

57−> so (ass `isPartition` union ass)

57+> So (ass `isPartition` union ass)

58> partitionLemma0 ass asspd = (soAndIntro (\ xss => arePairwiseDisjoint xss)

59> (\ xs => union ass == xs)

60> ass

61> (union ass)

62> asspd

63> uasseqas) where

64−> uasseqas : so (union ass == union ass)

64+> uasseqas : So (union ass == union ass)

65> uasseqas = reflexive_Set_eqeq (union ass)

66

test/reg044/reg044.idr+1−1

@@ -3,4 +3,4 @@ exjection = ?pf

3

4pf = proof

5 intros

6− refine refl

6+ refine Refl

test/reg047/reg047.idr+3−3

@@ -8,11 +8,11 @@ data Nat = zero | succ Nat

8Id : (A : Type) -> A -> A -> Type

9Id A = (=) {a0 = A} {b0 = A}

10

11−Refl : (A : Type) -> (a : A) -> Id A a a

11+IdRefl : (A : Type) -> (a : A) -> Id A a a

12−Refl A a = refl {a}

12+IdRefl A a = Refl {a}

13

14zzz : Id Nat zero zero

15−zzz = Refl Nat zero

15+zzz = IdRefl Nat zero

16

17eep : TTSigma Nat (\ a => Id Nat a zero)

18eep = sigma Nat (\ a => Id Nat a zero) zero zzz

test/reg047/reg047a.idr+4−4

@@ -8,17 +8,17 @@ data MNat = zero | succ MNat

8Id : (A : Type) -> A -> A -> Type

9Id = \A,x,y => x = y -- {a = A} {b = A}

10

11−Refl : (A : Type) -> (a : A) -> Id A a a

11+IdRefl : (A : Type) -> (a : A) -> Id A a a

12−Refl A a = refl {a}

12+IdRefl A a = Refl {a}

13

14zzzz : Id MNat zero zero

15−zzzz = Refl MNat zero

15+zzzz = IdRefl MNat zero

16

17eep : TTSigma MNat (\ c => Id MNat c zero)

18eep = (sigma MNat (\b => Id MNat b zero) zero zzzz)

19

20eep2 : TTSigma MNat (\ c => Id MNat c zero)

21−eep2 = (sigma MNat (\b => Id MNat b zero) zero (Refl MNat zero))

21+eep2 = (sigma MNat (\b => Id MNat b zero) zero (IdRefl MNat zero))

22

23

24

test/totality002/test017.idr+3−3

@@ -82,9 +82,9 @@ mfib (S (S n)) = mfib (S n) + mfib n

82

83maxCommutative : (left : Nat) -> (right : Nat) ->

84 maximum left right = maximum right left

85−maxCommutative Z Z = refl

85+maxCommutative Z Z = Refl

86−maxCommutative (S left) Z = refl

86+maxCommutative (S left) Z = Refl

87−maxCommutative Z (S right) = refl

87+maxCommutative Z (S right) = Refl

88maxCommutative (S left) (S right) =

89 let inductiveHypothesis = maxCommutative left right in

90 ?maxCommutativeStepCase

test/totality006/expected+1−1

@@ -1,2 +1,2 @@

1totality006.idr:6:1:Main.prf is not total as there are missing cases

2−totality006a.idr:9:6:prf' (S _) (S _) oh is a valid case

2+totality006a.idr:9:6:prf' (S _) (S _) Oh is a valid case

test/totality006/totality006.idr+6−6

@@ -1,11 +1,11 @@

1−antitrue : so False -> a

1+antitrue : So False -> a

2−antitrue oh impossible

2+antitrue Oh impossible

3

4total

5−prf : (a:Nat) -> (b:Nat) -> so (a > b) -> GT a b

5+prf : (a:Nat) -> (b:Nat) -> So (a > b) -> GT a b

6−prf Z Z oh impossible

6+prf Z Z Oh impossible

7prf Z (S k) um = antitrue um

8−prf (S k) Z um = lteSucc lteZero

8+prf (S k) Z um = LTESucc LTEZero

9−-- prf (S _) (S _) oh impossible

9+-- prf (S _) (S _) Oh impossible

10

11

test/totality006/totality006a.idr+6−6

@@ -1,10 +1,10 @@

1−antitrue : so False -> a

1+antitrue : So False -> a

2−antitrue oh impossible

2+antitrue Oh impossible

3

4total

5−prf' : (a:Nat) -> (b:Nat) -> so (a > b) -> GT a b

5+prf' : (a:Nat) -> (b:Nat) -> So (a > b) -> GT a b

6−prf' Z Z oh impossible

6+prf' Z Z Oh impossible

7prf' Z (S k) um = antitrue um

8−prf' (S k) Z um = lteSucc lteZero

8+prf' (S k) Z um = LTESucc LTEZero

9−prf' (S _) (S _) oh impossible

9+prf' (S _) (S _) Oh impossible

10

test/tutorial004/tutorial004.idr+5−5

@@ -1,9 +1,9 @@

1

2fiveIsFive : 5 = 5

3−fiveIsFive = refl

3+fiveIsFive = Refl

4

5twoPlusTwo : 2 + 2 = 4

6−twoPlusTwo = refl

6+twoPlusTwo = Refl

7

8total disjoint : (n : Nat) -> Z = S n -> _|_

9disjoint n p = replace {P = disjointTy} p ()

@@ -25,14 +25,14 @@ empty2 : _|_

25empty2 = empty2

26

27plusReduces : (n:Nat) -> plus Z n = n

28−plusReduces n = refl

28+plusReduces n = Refl

29

30plusReducesZ : (n:Nat) -> n = plus n Z

31−plusReducesZ Z = refl

31+plusReducesZ Z = Refl

32plusReducesZ (S k) = cong (plusReducesZ k)

33

34plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)

35−plusReducesS Z m = refl

35+plusReducesS Z m = Refl

36plusReducesS (S k) m = cong (plusReducesS k m)

37

38plusReducesZ' : (n:Nat) -> n = plus n Z