f0ed9e9 · Idris-dev · git.iko.soy

benchmarks/quasigroups/Solver.idr+4−4

compare with master

unifiedsplit

@@ -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

@@ -128,13 +128,13 @@ CompleteBoard : Board n -> Type

128CompleteBoard b = (LegalBoard b, FullBoard b)

129

130indexStep : {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''))) =>

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+33−33

@@ -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 _|_) ()

@@ -274,11 +274,11 @@ maybeIsoS = MkIso forth back fb bf

274 back fZ = Nothing

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/BoundedList.idr+1−1

@@ -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/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+5−5

@@ -15,7 +15,7 @@ import Decidable.Equality

15

16class Preorder t (po : t -> t -> Type) where

17 total transitive : (a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c

18− total reflexive : (a : t) -> po a a

18+ total Reflexive : (a : t) -> po a a

19

20class (Preorder t po) => Poset t (po : t -> t -> Type) where

21 total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b

@@ -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

@@ -76,11 +76,11 @@ NatLTEIsReflexive _ = nEqn

76

77instance Preorder Nat NatLTE where

78 transitive = NatLTEIsTransitive

79− reflexive = NatLTEIsReflexive

79+ Reflexive = NatLTEIsReflexive

80

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

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

83−NatLTEIsAntisymmetric n n nEqn nEqn = refl

83+NatLTEIsAntisymmetric n n nEqn nEqn = Refl

84NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible

85NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible

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

@@ -145,7 +145,7 @@ using (k : Nat)

145 instance Preorder (Fin k) FinLTE where

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

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

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

148+ Reflexive n = FromNatPrf (NatLTEIsReflexive (finToNat n))

149

150 instance Poset (Fin k) FinLTE where

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

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/prelude/Builtins.idr+19−4

@@ -3,11 +3,26 @@

3%access public

4%default total

5

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

7+||| true proposition.

8+data Unit =

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

10+ MkUnit

11+

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

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

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

15+data Pair : (A : Type) -> (B : Type) -> Type =

16+ ||| A pair of elements

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

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

19+ MkPair : (a : A) -> (b : B) -> Pair A B

20+

6||| Dependent pairs, in their internal representation

21||| Dependent pairs, in their internal representation

7||| @ a the type of the witness

22||| @ a the type of the witness

8||| @ P the type of the proof

23||| @ P the type of the proof

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

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

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

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

11

26

12||| The eliminator for the empty type.

27||| The eliminator for the empty type.

13FalseElim : _|_ -> a

28FalseElim : _|_ -> a

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

32|||

47|||

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

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

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

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

35−replace refl prf = prf

50+replace Refl prf = prf

36

51

37||| Symmetry of propositional equality

52||| Symmetry of propositional equality

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

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

39−sym refl = refl

54+sym Refl = Refl

40

55

41||| Transitivity of propositional equality

56||| Transitivity of propositional equality

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

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

43−trans refl refl = refl

58+trans Refl Refl = Refl

44

59

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

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

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

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

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

@@ -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')

@@ -97,10 +97,10 @@ instance (DecEq a, DecEq b) => DecEq (Either a b) where

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

98

99total 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

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

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

@@ -112,24 +112,24 @@ instance DecEq (Fin n) where

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/Basics.idr+1−1

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

42

43||| Equality is a congruence.

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

45−cong refl = refl

45+cong Refl = Refl

46

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

48data Dec : Type -> Type where

libs/prelude/Prelude/Classes.idr+2

@@ -28,8 +28,10 @@ class Eq a where

28 x /= y = not (x == y)

29 x == y = not (x /= y)

30

31+%logging 5

31instance Eq () where

32instance Eq () where

32 () == () = True

33 () == () = True

34+%logging 0

33

35

34instance Eq Int where

36instance Eq Int where

35 (==) = boolOp prim__eqInt

37 (==) = boolOp prim__eqInt

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

@@ -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+5−5

@@ -20,7 +20,7 @@ instance Uninhabited (Fin Z) where

20 uninhabited (fS f) impossible

21

22fSInjective : (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

@@ -41,9 +41,9 @@ 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

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

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

49

@@ -90,7 +90,7 @@ last {n=Z} = fZ

90last {n=S _} = fS last

91

92total 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

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+91−91

@@ -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

@@ -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

629total 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/Vect.idr+5−5

@@ -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

@@ -470,15 +470,15 @@ transpose (x :: xs) = zipWith (::) x (transpose xs)

470--------------------------------------------------------------------------------

471

472vectConsCong : (x : a) -> (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> (x :: xs = x :: ys)

473−vectConsCong x xs xs refl = refl

473+vectConsCong x xs xs Refl = Refl

474

475vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs

476−vectNilRightNeutral [] = refl

476+vectNilRightNeutral [] = Refl

477vectNilRightNeutral (x :: xs) =

478 vectConsCong _ _ _ (vectNilRightNeutral xs)

479

480vectAppendAssociative : (x : Vect xLen a) -> (y : Vect yLen a) -> (z : Vect zLen a) -> x ++ (y ++ z) = (x ++ y) ++ z

481−vectAppendAssociative [] y z = refl

481+vectAppendAssociative [] y z = Refl

482vectAppendAssociative (x :: xs) ys zs =

483 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)

484

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)))

src/Idris/AbsSyntaxTree.hs+9−16

@@ -496,7 +496,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying

496 | CExport String -- export, with a C name

497 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension

498 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error

499− | Reflection -- a reflecting function, compile-time only

499+ | Reflection -- a Reflecting function, compile-time only

500 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names

501 | Constructor -- Data constructor type

502 deriving (Show, Eq)

@@ -1063,15 +1063,15 @@ 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

1068primNames = [unitTy, unitCon,

1069 falseTy, pairTy, pairCon,

1070 eqTy, eqCon, inferTy, inferCon]

1071

1072unitDoc = parseDocstring . T.pack $ "The canonical single-element type, also known as the trivially true proposition."

1073−unitTy = sMN 0 "__Unit"

1073+unitTy = sUN "Unit"

1074−unitCon = sMN 0 "__II"

1074+unitCon = sUN "MkUnit"

1075unitDecl = PDatadecl unitTy PType

1076 [(parseDocstring . T.pack $ "The trivial constructor for `()`. ", [], unitCon, PRef bi unitTy, bi, [])]

1077unitOpts = [DefaultEliminator]

@@ -1086,8 +1086,8 @@ falseDecl = PDatadecl falseTy PType []

1086falseOpts = []

1087

1088pairDoc = parseDocstring . T.pack $ "The non-dependent pair type, also known as conjunction."

1089−pairTy = sMN 0 "__Pair"

1089+pairTy = sUN "Pair"

1090−pairCon = sMN 0 "__MkPair"

1090+pairCon = sUN "MkPair"

1091pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

1092 [(pairConDoc, pairConParamDoc,

1093 pairCon, PPi impl (n "A") PType (

@@ -1106,7 +1106,7 @@ pairParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left elements

1106 where n a = sMN 0 a

1107

1108eqTy = sUN "="

1109−eqCon = sUN "refl"

1109+eqCon = sUN "Refl"

1110eqDoc = parseDocstring . T.pack $

1111 "The propositional equality type. A proof that `x` = `y`." ++

1112 "\n\n" ++

@@ -1143,16 +1143,9 @@ eqParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left side of th

1143

1144eqOpts = []

1145

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

1146-- Defined in builtins.idr

1154sigmaTy = sUN "Sigma"

1147sigmaTy = sUN "Sigma"

1155−existsCon = sUN "Sg_intro"

1148+existsCon = sUN "MkSigma"

1156

1149

1157piBind :: [(Name, PTerm)] -> PTerm -> PTerm

1150piBind :: [(Name, PTerm)] -> PTerm -> PTerm

1158piBind = piBindp expl

1151piBind = piBindp expl

@@ -1338,7 +1331,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1338

1331

1339 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r

1332 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

1333 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm

1341− prettySe p bnd (PRefl _ _) = annName eqCon $ text "refl"

1334+ prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"

1342 prettySe p bnd (PResolveTC _) = text "resolvetc"

1335 prettySe p bnd (PResolveTC _) = text "resolvetc"

1343 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"

1336 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"

1344 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

1337 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−1

@@ -81,7 +81,6 @@ elabPrims = do mapM_ (elabDecl' EAll recinfo)

81 [emptyDocstring, unitDoc, falseDoc, pairDoc, eqDoc]

82 [[], [], [], pairParamDoc, 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/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/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/dsl003/DSLPi.idr+2−2

@@ -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 ===

@@ -35,4 +35,4 @@ test3 : Spec []

35test3 = ForAll INT . ForAll INT . ItHolds $ Var (fS fZ) === Var fZ

36

37test4 : test2 = test3

38−test4 = refl

38+test4 = Refl

test/dsl003/expected+1−1

@@ -1,2 +1,2 @@

1ForAll 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/error004/FunErrTest.idr+4−4

@@ -11,12 +11,12 @@ 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

19−extractList (App (App reflCon (App isCons lst)) _) = Just lst

19+extractList (App (App ReflCon (App isCons lst)) _) = Just lst

20extractList _ = Nothing

21

22total

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/primitives003/test038.idr+1−1

@@ -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 ()

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+32−32

@@ -9,7 +9,7 @@ using (xs : List a, ys : List a, G : List (List a))

9 Stop : Elem x (x :: xs)

10 Pop : Elem x ys -> Elem x (y :: xs)

11

12−-- Expr is a reflection of a list, indexed over the concrete list,

12+-- Expr is a Reflection of a list, indexed over the concrete list,

13-- and over a set of list variables.

14

15 data Expr : List (List a) -> List a -> Type where

@@ -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,22 +68,22 @@ 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

79+-- Given a couple of Reflected expressions, try to produce a proof that

80-- they are equal

81

82 buildProof : {xs : List a} -> {ys : 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)

@@ -91,7 +91,7 @@ using (xs : List a, ys : List a, G : List (List a))

91 let (rn ** (r', rPrf)) = reduce r in

92 buildProof l' r' lPrf rPrf

93

94−-- Given a reflected equality, try to produce a proof that holds

94+-- Given a Reflected equality, try to produce a proof that holds

95

96 prove : ListEq G t -> Maybe t

97 prove (EqP xs ys) = testEq xs ys

@@ -103,12 +103,12 @@ using (xs : List a, ys : List a, G : List (List a))

103-- Some helpers for later... 'prim__syntactic_eq' is a primitive which

104-- (at compile-time only) attempts to construct a proof that its arguments

105-- are syntactically equal. We'll find this useful for referring to variables

106−-- in reflected terms.

106+-- in Reflected terms.

107

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)

@@ -122,44 +122,44 @@ using (xs : List a, ys : List a, G : List (List a))

122 weaken G' ENil = ENil

123

124

125−-- Now, some reflection magic.

125+-- Now, some Reflection magic.

126−-- %reflection means a function runs on syntax, rather than on constructors.

126+-- %Reflection means a function runs on syntax, rather than on constructors.

127−-- So, 'reflectList' builds a reflected List expression as defined above.

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

132+%Reflection

133−reflectList : (G : List (List a)) ->

133+ReflectList : (G : List (List a)) ->

134 (xs : List a) -> (G' ** Expr (G' ++ G) xs)

135−reflectList G [] = ([] ** ENil)

135+ReflectList G [] = ([] ** ENil)

136

137−reflectList G (x :: xs) with (reflectList G xs)

137+ReflectList G (x :: xs) with (ReflectList G xs)

138 | (G' ** xs') with (isElem (List.(::) x []) (G' ++ G))

139 | Just p = (G' ** App (Var p) xs')

140 | Nothing = ([x] :: G' ** App (Var Stop) (weaken [[x]] xs'))

141

142−reflectList G (xs ++ ys) with (reflectList G xs)

142+ReflectList G (xs ++ ys) with (ReflectList G xs)

143− | (G' ** xs') with (reflectList (G' ++ G) ys)

143+ | (G' ** xs') with (ReflectList (G' ++ G) ys)

144 | (G'' ** ys') = ((G'' ++ G') **

145 rewrite (sym (appendAssociative G'' G' G)) in

146 App (weaken G'' xs') ys')

147−reflectList G t with (isElem t G)

147+ReflectList G t with (isElem t G)

148 | Just p = ([] ** Var p)

149 | Nothing = ([t] ** Var Stop)

150

151

152−-- Similarly, reflectEq converts an equality proof on Lists into the ListEq

152+-- Similarly, ReflectEq converts an equality proof on Lists into the ListEq

153−-- reflection. Note that it isn't total, and we have to give the element type

153+-- Reflection. Note that it isn't total, and we have to give the element type

154-- explicitly because it can't be inferred from P.

155

156−-- This is not really a problem - we'll want different reflections for different

156+-- This is not really a problem - we'll want different Reflections for different

157-- forms of equality proofs anyway.

158

159−%reflection

159+%Reflection

160−reflectEq : (a : Type) -> (G : List (List a)) -> (P : Type) -> (G' ** ListEq (G' ++ G) P)

160+ReflectEq : (a : Type) -> (G : List (List a)) -> (P : Type) -> (G' ** ListEq (G' ++ G) P)

161−reflectEq a G (the (List a) xs = the (List a) ys) with (reflectList G xs)

161+ReflectEq a G (the (List a) xs = the (List a) ys) with (ReflectList G xs)

162− | (G' ** xs') with (reflectList (G' ++ G) ys)

162+ | (G' ** xs') with (ReflectList (G' ++ G) ys)

163 | (G'' ** ys') = ((G'' ++ G') **

164 rewrite (sym (appendAssociative G'' G' G)) in

165 EqP (weaken G'' xs') ys')

@@ -196,14 +196,14 @@ Reflect.bp1 = proof {

196

197-- "quoteGoal x by p in e" does some magic

198-- The effect is to bind x to p applied to the current goal. If 'p' is a

199−-- reflection function (which is the most likely thing to be useful...)

199+-- Reflection function (which is the most likely thing to be useful...)

200-- then we can feed the result to the above 'prove' function and pull out

201-- the proof, if it exists.

202

203-- The syntax declaration below just gives us an easy way to invoke the

204-- prover.

205

206−syntax AssocProof [ty] = quoteGoal x by reflectEq ty [] in

206+syntax AssocProof [ty] = quoteGoal x by ReflectEq ty [] in

207 getJust (prove (getProof x)) ItIsJust

208

209

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/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/reg012/reg012.lidr+4−4

@@ -12,10 +12,10 @@

12

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/reg025/reg025.idr+3−3

@@ -22,13 +22,13 @@ FullBoard : Board n -> Type

22FullBoard (MkBoard b) = All (All Filled) b

23

24indexStep : {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''))) =>

@@ -36,7 +36,7 @@ find {P} d (x::xs) with (d x)

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))

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/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+1−1

@@ -9,7 +9,7 @@ Id : (A : Type) -> A -> A -> Type

9Id A = (=) {a0 = A} {b0 = A}

10

11Refl : (A : Type) -> (a : A) -> Id A a a

12−Refl A a = refl {a}

12+Refl A a = Refl {a}

13

14zzz : Id Nat zero zero

15zzz = Refl Nat zero

test/reg047/reg047a.idr+1−1

@@ -9,7 +9,7 @@ Id : (A : Type) -> A -> A -> Type

9Id = \A,x,y => x = y -- {a = A} {b = A}

10

11Refl : (A : Type) -> (a : A) -> Id A a a

12−Refl A a = refl {a}

12+Refl A a = Refl {a}

13

14zzzz : Id MNat zero zero

15zzzz = Refl MNat zero

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/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