git.iko.soy/Idris-dev
on master help sign in
Merge branch 'ahmadsalim-feature/renaming'
commit44cdd8a8fe51a696addc365d4e52b574576654b0 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 30 Sep 2014, 13:50 (12 years ago) parent45de9abcca0241
83 files changed+661−678
compare with master
unifiedsplit
CHANGELOG+1 benchmarks/quasigroups/Parser.idr+8−8 benchmarks/quasigroups/Solver.idr+14−14 contribs/gtksourceview-2.0-language-spec/idris.lang+1−1 libs/base/Control/Isomorphism.idr+37−37 libs/base/Control/Isomorphism/Primitives.idr+4−4 libs/base/Data/Bits.idr+2−2 libs/base/Data/BoundedList.idr+5−5 libs/base/Data/Buffer.idr+2−2 libs/base/Data/HVect.idr+9−9 libs/base/Data/Heap.idr+7−7 libs/base/Data/List.idr+2−2 libs/base/Data/Vect.idr+2−2 libs/base/Data/ZZ.idr+12−12 libs/base/Decidable/Order.idr+55−66 libs/base/Syntax/PreorderReasoning.idr+3−3 libs/base/System/Concurrency/Process.idr+13−13 libs/effects/Effect/Memory.idr+12−12 libs/prelude/Builtins.idr+20−4 libs/prelude/Decidable/Equality.idr+45−45 libs/prelude/Prelude.idr+3−3 libs/prelude/Prelude/Basics.idr+3−1 libs/prelude/Prelude/Bool.idr+4−3 libs/prelude/Prelude/Either.idr+6−6 libs/prelude/Prelude/Fin.idr+44−44 libs/prelude/Prelude/List.idr+20−20 libs/prelude/Prelude/Maybe.idr+1−1 libs/prelude/Prelude/Nat.idr+107−107 libs/prelude/Prelude/Pairs.idr+6−6 libs/prelude/Prelude/Strings.idr+2−2 libs/prelude/Prelude/Vect.idr+20−19 samples/binary.idr+1−1 samples/interp-alt.idr+13−13 samples/interp.idr+2−2 samples/reflection.idr+2−2 src/Idris/AbsSyntaxTree.hs+9−39 src/Idris/Apropos.hs+1−1 src/Idris/ElabDecls.hs+4−5 src/Idris/ElabTerm.hs+10−6 src/Idris/Erasure.hs+3−3 src/Idris/ParseExpr.hs+2−2 test/basic001/basic001a.idr+1−1 test/basic001/reg005.idr+2−2 test/basic005/test019.lidr+6−6 test/basic009/Faulty.idr+1−1 test/basic009/Main.idr+4−4 test/basic010/Main.idr+2−2 test/dsl001/test001.idr+3−3 test/dsl002/Resimp.idr+2−2 test/dsl003/DSLPi.idr+5−5 test/dsl003/expected+2−2 test/effects002/test025.idr+6−6 test/error004/FunErrTest.idr+3−3 test/ffi002/test023.idr+2−2 test/interactive001/expected+1−1 test/io003/test018a.idr+5−5 test/primitives003/test038.idr+5−5 test/proof001/test029.idr+2−2 test/proof002/Reflect.idr+9−9 test/proof003/test015.idr+1−1 test/quasiquote001/expected+3−3 test/quasiquote003/NoInfer.idr+2−2 test/quasiquote004/Quasiquote004.idr+1−1 test/reg002/reg002.idr+2−2 test/reg006/reg006.idr+3−3 test/reg007/reg007.lidr+1−1 test/reg009/reg009.lidr+6−6 test/reg012/reg012.lidr+11−11 test/reg017/reg017.idr+2−2 test/reg018/reg018d.idr+3−3 test/reg025/reg025.idr+7−7 test/reg026/reg026.idr+1−1 test/reg034/reg034.idr+2−2 test/reg035/reg035.idr+2−2 test/reg035/reg035a.lidr+7−7 test/reg044/reg044.idr+1−1 test/reg047/reg047.idr+3−3 test/reg047/reg047a.idr+4−4 test/totality002/test017.idr+3−3 test/totality006/expected+1−1 test/totality006/totality006.idr+6−6 test/totality006/totality006a.idr+6−6 test/tutorial004/tutorial004.idr+5−5
CHANGELOG+1
@@ -20,6 +20,7 @@ New in 0.9.15:
2020 compiler distribution only ships with the C and JavaScript backends.
2121* New REPL command :printdef displays the internal definition of a name
2222* 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)
2324
2425New in 0.9.14:
2526--------------
benchmarks/quasigroups/Parser.idr+8−8
@@ -24,11 +24,11 @@ parseToken x = map Just (tryParseFin ((cast x) - 1))
2424 where
2525 tryParseFin : Int -> Either String (Fin n)
2626 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
2828 tryParseFin {n=S k} x =
2929 case tryParseFin {n=k} (x-1) of
3030 Left err => Left err
31− Right fin => return (fS fin)
31+ Right fin => return (FS fin)
3232
3333length : Vect n a -> Nat
3434length {n=n} _ = n
@@ -49,9 +49,9 @@ parseCols {n=S k} row l cs = helper last l
4949 No _ => Left ("Illegal cell " ++ index x cs)
5050
5151 helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)
52− helper fZ l = step l fZ
53− helper (fS k) l = do
54− (_ ** next) <- step l (fS k)
52+ helper FZ l = step l FZ
53+ helper (FS k) l = do
54+ (_ ** next) <- step l (FS k)
5555 helper (weaken k) next
5656
5757parseRows : (b : Board n) -> LegalBoard b -> Vect n String -> Parser n
@@ -66,9 +66,9 @@ parseRows {n=S k} _ l rs = helper last l
6666 Yes prf => let foo = (replace {P=\n => Vect n String} prf cs) in parseCols i l foo -- TODO: foo shouldn't be needed
6767
6868 helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)
69− helper fZ l = step fZ l
70− helper (fS k) l = do
71− (_ ** next) <- step (fS k) l
69+ helper FZ l = step FZ l
70+ helper (FS k) l = do
71+ (_ ** next) <- step (FS k) l
7272 helper (weaken k) next
7373
7474parse : 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
3535 show (MkBoard rs) = unlines (map showRow rs)
3636
3737updateAt : Fin n -> Vect n a -> (a -> a) -> Vect n a
38−updateAt fZ (x::xs) f = f x :: xs
39−updateAt (fS i) (x::xs) f = x :: updateAt i xs f
38+updateAt FZ (x::xs) f = f x :: xs
39+updateAt (FS i) (x::xs) f = x :: updateAt i xs f
4040
4141setCell : Board n -> (Fin n, Fin n) -> Fin n -> Board n
4242setCell (MkBoard b) (x, y) value = MkBoard (updateAt y b (\row => updateAt x row (const (Just value))))
@@ -80,7 +80,7 @@ Empty : Cell n -> Type
8080Empty {n=n} x = (the (Cell n) Nothing) = x
8181
8282empty : (cell : Cell n) -> Dec (Empty cell)
83−empty Nothing = Yes refl
83+empty Nothing = Yes Refl
8484empty (Just _) = No nothingNotJust
8585
8686-- Predicate for legal cell assignments
@@ -107,7 +107,7 @@ Filled {n=n} = (\x => Not (Empty x))
107107--Filled {n=n} = \x => the (Maybe (Fin n)) Nothing = x -> _|_
108108
109109filled : (cell : Cell n) -> Dec (Filled cell)
110−filled Nothing = No (\f => f refl)
110+filled Nothing = No (\f => f Refl)
111111filled (Just _) = Yes nothingNotJust
112112
113113FullBoard : Board n -> Type
@@ -127,18 +127,18 @@ data LegalBoard : Board n -> Type where
127127CompleteBoard : Board n -> Type
128128CompleteBoard b = (LegalBoard b, FullBoard b)
129129
130−indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (fS i) (x::xs)
131−indexStep = refl
130+indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (FS i) (x::xs)
131+indexStep = Refl
132132
133133find : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a)
134134 -> Either (All (\x => Not (P x)) xs) (y : a ** (P y, (i : Fin n ** y = index i xs)))
135135find _ Nil = Left Nil
136136find d (x::xs) with (d x)
137− | Yes prf = Right (x ** (prf, (fZ ** refl)))
137+ | Yes prf = Right (x ** (prf, (FZ ** Refl)))
138138 | No prf =
139139 case find d xs of
140140 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'')))
142142 Left prf' => Left (prf::prf')
143143
144144findEmptyInRow : (xs : Vect n (Cell n)) -> Either (All Filled xs) (i : Fin n ** Empty (index i xs))
@@ -158,11 +158,11 @@ emptyCell (MkBoard rs) =
158158 helper Nil = Left Nil
159159 helper (r::rs) =
160160 case findEmptyInRow r of
161− Right (ci ** pf) => Right (fZ ** (ci ** pf))
161+ Right (ci ** pf) => Right (FZ ** (ci ** pf))
162162 Left prf =>
163163 case helper rs of
164164 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))
166166
167167
168168tryValue : {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)
189189 Right success => (v, Just success)
190190 Left _ => -- TODO: Prove unsolvable
191191 case v of
192− fS k => tryAll (weaken k)
193− fZ => (v, Nothing)
192+ FS k => tryAll (weaken k)
193+ FZ => (v, Nothing)
194194
195195 %assert_total
196196 recurse : Fin (S n) -> Maybe (b' : Board (S n) ** CompleteBoard b')
197197 recurse start =
198198 case tryAll start of
199199 (_, Nothing) => Nothing
200− (fZ, Just (b' ** l')) => fillBoard b' l'
201− (fS next, Just (b' ** l')) =>
200+ (FZ, Just (b' ** l')) => fillBoard b' l'
201+ (FS next, Just (b' ** l')) =>
202202 case fillBoard b' l' of
203203 Just solution => Just solution
204204 Nothing => recurse (weaken next)
contribs/gtksourceview-2.0-language-spec/idris.lang+1−1
@@ -216,7 +216,7 @@
216216 <keyword>compute</keyword>
217217 <keyword>solve</keyword>
218218 <keyword>attack</keyword>
219− <keyword>refl</keyword>
219+ <keyword>Refl</keyword>
220220 <keyword>state</keyword>
221221 <keyword>term</keyword>
222222 <keyword>undo</keyword>
libs/base/Control/Isomorphism.idr+37−37
@@ -14,9 +14,9 @@ data Iso : Type -> Type -> Type where
1414
1515-- Isomorphism properties
1616
17−||| Isomorphism is reflexive
17+||| Isomorphism is Reflexive
1818isoRefl : Iso a a
19−isoRefl = MkIso id id (\x => refl) (\x => refl)
19+isoRefl = MkIso id id (\x => Refl) (\x => Refl)
2020
2121||| Isomorphism is transitive
2222isoTrans : Iso a b -> Iso b c -> Iso a c
@@ -43,8 +43,8 @@ eitherComm = MkIso swap swap swapSwap swapSwap
4343 swap (Left x) = Right x
4444 swap (Right x) = Left x
4545 swapSwap : (e : Either a' b') -> swap (swap e) = e
46− swapSwap (Left x) = refl
47− swapSwap (Right x) = refl
46+ swapSwap (Left x) = Refl
47+ swapSwap (Right x) = Refl
4848
4949||| Disjunction is associative
5050eitherAssoc : Iso (Either (Either a b) c) (Either a (Either b c))
@@ -60,14 +60,14 @@ eitherAssoc = MkIso eitherAssoc1 eitherAssoc2 ok1 ok2
6060 eitherAssoc2 (Right (Right x)) = Right x
6161
6262 ok1 : (x : Either a (Either b c)) -> eitherAssoc1 (eitherAssoc2 x) = x
63− ok1 (Left x) = refl
64− ok1 (Right (Left x)) = refl
65− ok1 (Right (Right x)) = refl
63+ ok1 (Left x) = Refl
64+ ok1 (Right (Left x)) = Refl
65+ ok1 (Right (Right x)) = Refl
6666
6767 ok2 : (x : Either (Either a b) c) -> eitherAssoc2 (eitherAssoc1 x) = x
68− ok2 (Left (Left x)) = refl
69− ok2 (Left (Right x)) = refl
70− ok2 (Right x) = refl
68+ ok2 (Left (Left x)) = Refl
69+ ok2 (Left (Right x)) = Refl
70+ ok2 (Right x) = Refl
7171
7272||| Disjunction with false is a no-op
7373eitherBotLeft : Iso (Either _|_ a) a
@@ -78,10 +78,10 @@ eitherBotLeft = MkIso to from ok1 ok2
7878 from : a -> Either _|_ a
7979 from = Right
8080 ok1 : (x : a) -> to (from x) = x
81− ok1 x = refl
81+ ok1 x = Refl
8282 ok2 : (x : Either _|_ a) -> from (to x) = x
8383 ok2 (Left x) = FalseElim x
84− ok2 (Right x) = refl
84+ ok2 (Right x) = Refl
8585
8686||| Disjunction with false is a no-op
8787eitherBotRight : Iso (Either a _|_) a
@@ -119,7 +119,7 @@ pairComm = MkIso swap swap swapSwap swapSwap
119119 swap (x, y) = (y, x)
120120
121121 swapSwap : (x : (a', b')) -> swap (swap x) = x
122− swapSwap (x, y) = refl
122+ swapSwap (x, y) = Refl
123123
124124||| Conjunction is associative
125125pairAssoc : Iso (a, (b, c)) ((a, b), c)
@@ -130,15 +130,15 @@ pairAssoc = MkIso to from ok1 ok2
130130 from : ((a, b), c) -> (a, (b, c))
131131 from ((x, y), z) = (x, (y, z))
132132 ok1 : (x : ((a, b), c)) -> to (from x) = x
133− ok1 ((x, y), z) = refl
133+ ok1 ((x, y), z) = Refl
134134 ok2 : (x : (a, (b, c))) -> from (to x) = x
135− ok2 (x, (y, z)) = refl
135+ ok2 (x, (y, z)) = Refl
136136
137137||| Conjunction with truth is a no-op
138138pairUnitRight : Iso (a, ()) a
139−pairUnitRight = MkIso fst (\x => (x, ())) (\x => refl) ok
139+pairUnitRight = MkIso fst (\x => (x, ())) (\x => Refl) ok
140140 where ok : (x : (a, ())) -> (fst x, ()) = x
141− ok (x, ()) = refl
141+ ok (x, ()) = Refl
142142
143143||| Conjunction with truth is a no-op
144144pairUnitLeft : Iso ((), a) a
@@ -165,11 +165,11 @@ pairCong {a = a} {a' = a'} {b = b} {b' = b'}
165165 iso1 : (x : (a', b')) -> to'' (from'' x) = x
166166 iso1 (x, y) = rewrite toFrom x in
167167 rewrite toFrom' y in
168− refl
168+ Refl
169169 iso2 : (x : (a, b)) -> from'' (to'' x) = x
170170 iso2 (x, y) = rewrite fromTo x in
171171 rewrite fromTo' y in
172− refl
172+ Refl
173173
174174||| Isomorphism is a congruence with regards to conjunction on the left
175175pairCongLeft : Iso a a' -> Iso (a, b) (a', b)
@@ -190,11 +190,11 @@ distribLeft = MkIso to from toFrom fromTo
190190 from (Left (x, y)) = (Left x, y)
191191 from (Right (x, y)) = (Right x, y)
192192 toFrom : (x : Either (a, c) (b, c)) -> to (from x) = x
193− toFrom (Left (x, y)) = refl
194− toFrom (Right (x, y)) = refl
193+ toFrom (Left (x, y)) = Refl
194+ toFrom (Right (x, y)) = Refl
195195 fromTo : (x : (Either a b, c)) -> from (to x) = x
196− fromTo (Left x, y) = refl
197− fromTo (Right x, y) = refl
196+ fromTo (Left x, y) = Refl
197+ fromTo (Right x, y) = Refl
198198
199199||| Products distribute over sums
200200distribRight : Iso (a, Either b c) (Either (a, b) (a, c))
@@ -217,10 +217,10 @@ step a iso1 iso2 = isoTrans iso1 iso2
217217maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)
218218maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2
219219 where ok1 : (y : Maybe b) -> map to (map from y) = y
220− ok1 Nothing = refl
220+ ok1 Nothing = Refl
221221 ok1 (Just x) = (Just (to (from x))) ={ cong (toFrom x) }= (Just x) QED
222222 ok2 : (x : Maybe a) -> map from (map to x) = x
223− ok2 Nothing = refl
223+ ok2 Nothing = Refl
224224 ok2 (Just x) = (Just (from (to x))) ={ cong (fromTo x) }= (Just x) QED
225225
226226||| `Maybe a` is the same as `Either a ()`
@@ -233,11 +233,11 @@ maybeEither = MkIso to from iso1 iso2
233233 from (Left x) = Just x
234234 from (Right ()) = Nothing
235235 iso1 : (x : Either a ()) -> to (from x) = x
236− iso1 (Left x) = refl
237− iso1 (Right ()) = refl
236+ iso1 (Left x) = Refl
237+ iso1 (Right ()) = Refl
238238 iso2 : (y : Maybe a) -> from (to y) = y
239− iso2 Nothing = refl
240− iso2 (Just x) = refl
239+ iso2 Nothing = Refl
240+ iso2 (Just x) = Refl
241241
242242||| Maybe of void is just unit
243243maybeVoidUnit : Iso (Maybe _|_) ()
@@ -268,17 +268,17 @@ eitherMaybeRightMaybe {a} {b} =
268268maybeIsoS : Iso (Maybe (Fin n)) (Fin (S n))
269269maybeIsoS = MkIso forth back fb bf
270270 where forth : Maybe (Fin n) -> Fin (S n)
271− forth Nothing = fZ
272− forth (Just x) = fS x
271+ forth Nothing = FZ
272+ forth (Just x) = FS x
273273 back : Fin (S n) -> Maybe (Fin n)
274− back fZ = Nothing
275− back (fS x) = Just x
274+ back FZ = Nothing
275+ back (FS x) = Just x
276276 bf : (x : Maybe (Fin n)) -> back (forth x) = x
277− bf Nothing = refl
278− bf (Just x) = refl
277+ bf Nothing = Refl
278+ bf (Just x) = Refl
279279 fb : (y : Fin (S n)) -> forth (back y) = y
280− fb fZ = refl
281− fb (fS x) = refl
280+ fb FZ = Refl
281+ fb (FS x) = Refl
282282
283283finZeroBot : Iso (Fin 0) _|_
284284finZeroBot = MkIso (\x => FalseElim (uninhabited x))
libs/base/Control/Isomorphism/Primitives.idr+4−4
@@ -20,16 +20,16 @@ integerIsoZZ = MkIso toZZ fromZZ fromToZZ toFromZZ
2020 fromZZ n = cast n
2121
2222 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
2424
2525 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
2727
2828
2929packUnpackIso : Iso (List Char) String
3030packUnpackIso = MkIso pack
3131 unpack
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)
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)
3434
3535
libs/base/Data/Bits.idr+2−2
@@ -437,8 +437,8 @@ bitsToStr x = pack (helper last x)
437437 where
438438 %assert_total
439439 helper : Fin (S n) -> Bits n -> List Char
440− helper fZ _ = []
441− helper (fS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b
440+ helper FZ _ = []
441+ helper (FS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b
442442
443443instance Show (Bits n) where
444444 show = bitsToStr
libs/base/Data/BoundedList.idr+5−5
@@ -10,8 +10,8 @@ data BoundedList : Nat -> Type -> Type where
1010
1111||| Compute the length of a list.
1212length : BoundedList n a -> Fin (S n)
13−length [] = fZ
14−length (x :: xs) = fS (length xs)
13+length [] = FZ
14+length (x :: xs) = FS (length xs)
1515
1616--------------------------------------------------------------------------------
1717-- Indexing into bounded lists
@@ -19,8 +19,8 @@ length (x :: xs) = fS (length xs)
1919
2020index : Fin (S n) -> BoundedList n a -> Maybe a
2121index _ [] = Nothing
22−index fZ (x :: _) = Just x
23−index (fS f) (_ :: xs) = index f xs
22+index FZ (x :: _) = Just x
23+index (FS f) (_ :: xs) = index f xs
2424
2525--------------------------------------------------------------------------------
2626-- Adjusting bounds
@@ -90,5 +90,5 @@ pad {n=S n'} (x :: xs) padding = x :: pad {n=n'} xs padding
9090--------------------------------------------------------------------------------
9191
9292zeroBoundIsEmpty : (xs : BoundedList 0 a) -> xs = the (BoundedList 0 a) []
93−zeroBoundIsEmpty [] = refl
93+zeroBoundIsEmpty [] = Refl
9494zeroBoundIsEmpty (_ :: _) impossible
libs/base/Data/Buffer.idr+2−2
@@ -33,8 +33,8 @@ bitsFromNat Z = 0
3333bitsFromNat (S k) = 1 + bitsFromNat k
3434
3535bitsFromFin : Fin n -> Bits64
36−bitsFromFin fZ = 0
37−bitsFromFin (fS k) = 1 + bitsFromFin k
36+bitsFromFin FZ = 0
37+bitsFromFin (FS k) = 1 + bitsFromFin k
3838
3939||| Allocate an empty Buffer. The size hint can be used to avoid
4040||| 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
1313
1414||| Extract an element from an HVect
1515index : (i : Fin k) -> HVect ts -> index i ts
16−index fZ (x::xs) = x
17−index (fS j) (x::xs) = index j xs
16+index FZ (x::xs) = x
17+index (FS j) (x::xs) = index j xs
1818
1919deleteAt : (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)
20−deleteAt fZ (x::xs) = xs
21−deleteAt {l = S m} (fS j) (x::xs) = x :: deleteAt j xs
22−deleteAt {l = Z} (fS j) (x::xs) = absurd j
20+deleteAt FZ (x::xs) = xs
21+deleteAt {l = S m} (FS j) (x::xs) = x :: deleteAt j xs
22+deleteAt {l = Z} (FS j) (x::xs) = absurd j
2323deleteAt _ [] impossible
2424
2525replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts)
26−replaceAt fZ y (x::xs) = y::xs
27−replaceAt (fS j) y (x::xs) = x :: replaceAt j y xs
26+replaceAt FZ y (x::xs) = y::xs
27+replaceAt (FS j) y (x::xs) = x :: replaceAt j y xs
2828
2929updateAt : (i : Fin k) -> (index i ts -> t) -> HVect ts -> HVect (replaceAt i t ts)
30−updateAt fZ f (x::xs) = f x :: xs
31−updateAt (fS j) f (x::xs) = x :: updateAt j f xs
30+updateAt FZ f (x::xs) = f x :: xs
31+updateAt (FS j) f (x::xs) = x :: updateAt j f xs
3232
3333||| Append two `HVect`s.
3434(++) : HVect ts -> HVect us -> HVect (ts ++ us)
libs/base/Data/Heap.idr+7−7
@@ -83,11 +83,11 @@ insert e = merge $ singleton e
8383--------------------------------------------------------------------------------
8484
8585findMinimum : (h : MaxiphobicHeap a) -> (isEmpty h = False) -> a
86−findMinimum Empty refl impossible
86+findMinimum Empty Refl impossible
8787findMinimum (Node s l e r) p = e
8888
8989deleteMinimum : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> MaxiphobicHeap a
90−deleteMinimum Empty refl impossible
90+deleteMinimum Empty Refl impossible
9191deleteMinimum (Node s l e r) p = merge l r
9292
9393--------------------------------------------------------------------------------
@@ -96,7 +96,7 @@ deleteMinimum (Node s l e r) p = merge l r
9696
9797toList : Ord a => MaxiphobicHeap a -> List a
9898toList 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
100100 where
101101 %assert_total -- relies on deleteMinimum making heap smaller
102102 toList' : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> List a
@@ -143,20 +143,20 @@ absurdBoolDischarge p = replace {P = disjointTy} p ()
143143 disjointTy True = _|_
144144
145145total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z
146−isEmptySizeZero Empty p = refl
146+isEmptySizeZero Empty p = Refl
147147isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd
148148
149149total emptyHeapValid : Ord a => isValidHeap empty = True
150−emptyHeapValid = refl
150+emptyHeapValid = Refl
151151
152152total singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True
153−singletonHeapValid e = refl
153+singletonHeapValid e = Refl
154154
155155{-
156156total mergePreservesValidHeaps : Ord a => (left : MaxiphobicHeap a) ->
157157 (right : MaxiphobicHeap a) -> (leftValid : isValidHeap left = True) ->
158158 (rightValid : isValidHeap right = True) -> isValidHeap $ merge left right = True
159−mergePreservesValidHeaps Empty Empty lp rp = refl
159+mergePreservesValidHeaps Empty Empty lp rp = Refl
160160mergePreservesValidHeaps Empty (Node rs rl re rr) lp rp = rp
161161mergePreservesValidHeaps (Node ls ll le lr) Empty lp rp = lp
162162mergePreservesValidHeaps (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
1818isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
1919isElem x [] = No absurd
2020isElem 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
2222 isElem x (y :: xs) | (No contra) with (isElem x xs)
2323 isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)
2424 isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)
@@ -26,5 +26,5 @@ isElem x (y :: xs) with (decEq x y)
2626 mkNo : {xs' : List a} ->
2727 ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) ->
2828 Elem x' (y' :: xs') -> _|_
29− mkNo f g Here = f refl
29+ mkNo f g Here = f Refl
3030 mkNo f g (There x) = g x
libs/base/Data/Vect.idr+2−2
@@ -20,14 +20,14 @@ noEmptyElem Here impossible
2020
2121||| An item not in the head and not in the tail is not in the Vect at all
2222neitherHereNorThere : {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
2424neitherHereNorThere xneqy xninxs (There xinxs) = xninxs xinxs
2525
2626||| A decision procedure for Elem
2727isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)
2828isElem x [] = No noEmptyElem
2929isElem 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
3131 isElem x (y :: xs) | (No xneqy) with (isElem x xs)
3232 isElem x (y :: xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)
3333 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)
101101natMultZMult n m x h = cong h
102102
103103doubleNegElim : (z : ZZ) -> negZ (negZ z) = z
104−doubleNegElim (Pos Z) = refl
105−doubleNegElim (Pos (S n)) = refl
106−doubleNegElim (NegS Z) = refl
107−doubleNegElim (NegS (S n)) = refl
104+doubleNegElim (Pos Z) = Refl
105+doubleNegElim (Pos (S n)) = Refl
106+doubleNegElim (NegS Z) = Refl
107+doubleNegElim (NegS (S n)) = Refl
108108
109109-- Injectivity
110110posInjective : Pos n = Pos m -> n = m
111−posInjective refl = refl
111+posInjective Refl = Refl
112112
113113negSInjective : NegS n = NegS m -> n = m
114−negSInjective refl = refl
114+negSInjective Refl = Refl
115115
116116posNotNeg : Pos n = NegS m -> _|_
117−posNotNeg refl impossible
117+posNotNeg Refl impossible
118118
119119-- Decidable equality
120120instance DecEq ZZ where
@@ -129,16 +129,16 @@ instance DecEq ZZ where
129129
130130-- Plus
131131plusZeroLeftNeutralZ : (right : ZZ) -> 0 + right = right
132−plusZeroLeftNeutralZ (Pos n) = refl
133−plusZeroLeftNeutralZ (NegS n) = refl
132+plusZeroLeftNeutralZ (Pos n) = Refl
133+plusZeroLeftNeutralZ (NegS n) = Refl
134134
135135plusZeroRightNeutralZ : (left : ZZ) -> left + 0 = left
136136plusZeroRightNeutralZ (Pos n) = cong $ plusZeroRightNeutral n
137−plusZeroRightNeutralZ (NegS n) = refl
137+plusZeroRightNeutralZ (NegS n) = Refl
138138
139139plusCommutativeZ : (left : ZZ) -> (right : ZZ) -> (left + right = right + left)
140140plusCommutativeZ (Pos n) (Pos m) = cong $ plusCommutative n m
141−plusCommutativeZ (Pos n) (NegS m) = refl
142−plusCommutativeZ (NegS n) (Pos m) = refl
141+plusCommutativeZ (Pos n) (NegS m) = Refl
142+plusCommutativeZ (NegS n) (Pos m) = Refl
143143plusCommutativeZ (NegS n) (NegS m) = cong {f=NegS} $ cong {f=S} $ plusCommutative n m
144144
libs/base/Decidable/Order.idr+55−66
@@ -48,7 +48,7 @@ maximum x y with (order x y)
4848
4949instance Preorder t ((=) {A = t} {B = t}) where
5050 transitive a b c = trans {a = a} {b = b} {c = c}
51− reflexive a = refl
51+ reflexive a = Refl
5252
5353instance Equivalence t ((=) {A = t} {B = t}) where
5454 symmetric a b prf = sym prf
@@ -60,99 +60,88 @@ instance Congruence t f ((=) {A = t} {B = t}) where
6060-- Natural numbers
6161--------------------------------------------------------------------------------
6262
63−data NatLTE : Nat -> Nat -> Type where
64− nEqn : NatLTE n n
65− nLTESm : NatLTE n m -> NatLTE n (S m)
63+total LTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->
64+ LTE m n -> LTE n o ->
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)
6668
67−total NatLTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->
68− NatLTE m n -> NatLTE n o ->
69− NatLTE m o
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)
69+total LTEIsReflexive : (n : Nat) -> LTE n n
70+LTEIsReflexive Z = LTEZero
71+LTEIsReflexive (S n) = LTESucc (LTEIsReflexive n)
7372
74−total NatLTEIsReflexive : (n : Nat) -> NatLTE n n
75−NatLTEIsReflexive _ = nEqn
73+instance Preorder Nat LTE where
74+ transitive = LTEIsTransitive
75+ reflexive = LTEIsReflexive
7676
77−instance Preorder Nat NatLTE where
78− transitive = NatLTEIsTransitive
79− reflexive = NatLTEIsReflexive
77+total LTEIsAntisymmetric : (m : Nat) -> (n : Nat) ->
78+ LTE m n -> LTE n m -> m = n
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
8082
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
8783
88−instance Poset Nat NatLTE where
89− antisymmetric = NatLTEIsAntisymmetric
84+instance Poset Nat LTE where
85+ antisymmetric = LTEIsAntisymmetric
9086
91−total zeroNeverGreater : {n : Nat} -> NatLTE (S n) Z -> _|_
92−zeroNeverGreater {n} (nLTESm _) impossible
93−zeroNeverGreater {n} nEqn impossible
87+total zeroNeverGreater : {n : Nat} -> LTE (S n) Z -> _|_
88+zeroNeverGreater {n} LTEZero impossible
89+zeroNeverGreater {n} (LTESucc _) impossible
9490
95−total zeroAlwaysSmaller : {n : Nat} -> NatLTE Z n
96−zeroAlwaysSmaller {n = Z } = nEqn
97−zeroAlwaysSmaller {n = S k} = nLTESm (zeroAlwaysSmaller {n = k})
91+total zeroAlwaysSmaller : {n : Nat} -> LTE Z n
92+zeroAlwaysSmaller = LTEZero
9893
99−total
100−nGTSm : {n : Nat} -> {m : Nat} -> (NatLTE n m -> _|_) -> NatLTE n (S m) -> _|_
101−nGTSm disprf (nLTESm nLTEm) = FalseElim (disprf nLTEm)
102−nGTSm {n} {m} disprf (nEqn) impossible
94+total ltesuccinjective : {n : Nat} -> {m : Nat} -> (LTE n m -> _|_) -> LTE (S n) (S m) -> _|_
95+ltesuccinjective {n} {m} disprf (LTESucc nLTEm) = FalseElim (disprf nLTEm)
96+ltesuccinjective {n} {m} disprf LTEZero impossible
10397
104−total
105−decideNatLTE : (n : Nat) -> (m : Nat) -> Dec (NatLTE n m)
106−decideNatLTE Z Z = Yes nEqn
107−decideNatLTE (S x) Z = No zeroNeverGreater
108−decideNatLTE x (S y) with (decEq x (S y))
109− | Yes eq = rewrite eq in Yes nEqn
110− | No _ with (decideNatLTE x y)
111− | Yes nLTEm = Yes (nLTESm nLTEm)
112− | No nGTm = No (nGTSm nGTm)
113−
114−instance Decidable [Nat,Nat] NatLTE where
115− decide = decideNatLTE
98+
99+total decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTE n m)
100+decideLTE Z y = Yes LTEZero
101+decideLTE (S x) Z = No zeroNeverGreater
102+decideLTE (S x) (S y) with (decEq (S x) (S y))
103+ | Yes eq = rewrite eq in Yes (reflexive x)
104+ | No _ with (decideLTE x y)
105+ | Yes nLTEm = Yes (LTESucc nLTEm)
106+ | No nGTm = No (ltesuccinjective nGTm)
107+
108+instance Decidable [Nat,Nat] LTE where
109+ decide = decideLTE
116110
117111total
118−lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
119−lte m n = decide {ts = [Nat,Nat]} {p = NatLTE} m n
112+lte : (m : Nat) -> (n : Nat) -> Dec (LTE m n)
113+lte m n = decide {ts = [Nat,Nat]} {p = LTE} m n
120114
121115total
122−shift : (m : Nat) -> (n : Nat) -> NatLTE m n -> NatLTE (S m) (S n)
123−shift Z Z _ = nEqn
124−shift Z (S Z) _ = nLTESm nEqn
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
131− order Z n = Left zeroAlwaysSmaller
132− order m Z = Right zeroAlwaysSmaller
116+shift : (m : Nat) -> (n : Nat) -> LTE m n -> LTE (S m) (S n)
117+shift m n mLTEn = LTESucc mLTEn
118+
119+instance Ordered Nat LTE where
120+ order Z n = Left LTEZero
121+ order m Z = Right LTEZero
133122 order (S k) (S j) with (order k j)
134123 order (S k) (S j) | Left prf = Left (shift k j prf)
135124 order (S k) (S j) | Right prf = Right (shift j k prf)
136125
137−--------------------------------------------------------------------------------
138−-- Finite numbers
139−--------------------------------------------------------------------------------
126+----------------------------------------------------------------------------------
127+---- Finite numbers
128+----------------------------------------------------------------------------------
140129
141130using (k : Nat)
142131 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
144133
145134 instance Preorder (Fin k) FinLTE where
146135 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))
136+ FromNatPrf (LTEIsTransitive (finToNat m) (finToNat n) (finToNat o) p1 p2)
137+ reflexive n = FromNatPrf (LTEIsReflexive (finToNat n))
149138
150139 instance Poset (Fin k) FinLTE where
151140 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)
153142
154143 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))
156145 | Yes prf = Yes (FromNatPrf prf)
157146 | No disprf = No (\ (FromNatPrf prf) => disprf prf)
158147
libs/base/Syntax/PreorderReasoning.idr+3−3
@@ -1,6 +1,6 @@
11module Syntax.PreorderReasoning
22
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.
44syntax [expr] "QED" = qed expr
55-- foo ={ prf }= bar ={ prf' }= fnord QED
66-- 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
99namespace Equal
1010 using (a : Type, x : a, y : a, z : a)
1111 qed : (x : a) -> x = x
12− qed x = the (x = x) refl
12+ qed x = the (x = x) Refl
1313 step : (x : a) -> x = y -> (y = z) -> x = z
14− step x refl refl = refl
14+ step x Refl Refl = Refl
1515
libs/base/System/Concurrency/Process.idr+13−13
@@ -12,38 +12,38 @@ data ProcID msg = MkPID Ptr
1212||| Type safe message passing programs. Parameterised over the type of
1313||| message which can be send, and the return type.
1414data Process : (msgType : Type) -> Type -> Type where
15− lift : IO a -> Process msg a
15+ Lift : IO a -> Process msg a
1616
1717instance Functor (Process msg) where
18− map f (lift a) = lift (map f a)
18+ map f (Lift a) = Lift (map f a)
1919
2020instance Applicative (Process msg) where
21− pure = lift . return
22− (lift f) <$> (lift a) = lift (f <$> a)
21+ pure = Lift . return
22+ (Lift f) <$> (Lift a) = Lift (f <$> a)
2323
2424instance Monad (Process msg) where
25− (lift io) >>= k = lift (do x <- io
25+ (Lift io) >>= k = Lift (do x <- io
2626 case k x of
27− lift v => v)
27+ Lift v => v)
2828
2929run : Process msg x -> IO x
30−run (lift prog) = prog
30+run (Lift prog) = prog
3131
3232||| Get current process ID
3333myID : Process msg (ProcID msg)
34−myID = lift (return (MkPID prim__vm))
34+myID = Lift (return (MkPID prim__vm))
3535
3636||| Send a message to another process
3737send : 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))
3939
4040||| Return whether a message is waiting in the queue
4141msgWaiting : Process msg Bool
42−msgWaiting = lift checkMsgs
42+msgWaiting = Lift checkMsgs
4343
4444||| Receive a message - blocks if there is no message waiting
4545recv : Process msg msg
46−recv {msg} = do (senderid, m) <- lift get
46+recv {msg} = do (senderid, m) <- Lift get
4747 return m
4848 where get : IO (Ptr, msg)
4949 get = getMsg
@@ -51,11 +51,11 @@ recv {msg} = do (senderid, m) <- lift get
5151||| receive a message, and return with the sender's process ID.
5252recvWithSender : Process msg (ProcID msg, msg)
5353recvWithSender {msg}
54− = do (senderid, m) <- lift get
54+ = do (senderid, m) <- Lift get
5555 return (MkPID senderid, m)
5656 where get : IO (Ptr, msg)
5757 get = getMsg
5858
5959create : Process msg () -> Process msg (ProcID msg)
60−create (lift p) = do ptr <- lift (fork p)
60+create (Lift p) = do ptr <- Lift (fork p)
6161 return (MkPID ptr)
libs/effects/Effect/Memory.idr+12−12
@@ -16,23 +16,23 @@ data RawMemory : Effect where
1616 Free : RawMemory () (MemoryChunk n i) (\v => ())
1717 Initialize : Bits8 ->
1818 (size : Nat) ->
19− so (i + size <= n) ->
19+ So (i + size <= n) ->
2020 RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (i + size))
2121 Peek : (offset : Nat) ->
2222 (size : Nat) ->
23− so (offset + size <= i) ->
23+ So (offset + size <= i) ->
2424 RawMemory (Vect size Bits8)
2525 (MemoryChunk n i) (\v => MemoryChunk n i)
2626 Poke : (offset : Nat) ->
2727 (Vect size Bits8) ->
28− so (offset <= i && offset + size <= n) ->
28+ So (offset <= i && offset + size <= n) ->
2929 RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))
3030 Move : (src : MemoryChunk src_size src_init) ->
3131 (dst_offset : Nat) ->
3232 (src_offset : Nat) ->
3333 (size : Nat) ->
34− so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
35− so (src_offset + size <= src_init) ->
34+ So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
35+ So (src_offset + size <= src_init) ->
3636 RawMemory () (MemoryChunk dst_size dst_init)
3737 (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))
3838 GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)
@@ -108,7 +108,7 @@ initialize : {i : Nat} ->
108108 {n : Nat} ->
109109 Bits8 ->
110110 (size : Nat) ->
111− so (i + size <= n) ->
111+ So (i + size <= n) ->
112112 Eff () [RAW_MEMORY (MemoryChunk n i)]
113113 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])
114114initialize c size prf = call $ Initialize c size prf
@@ -119,7 +119,7 @@ free = call Free
119119peek : {i : Nat} ->
120120 (offset : Nat) ->
121121 (size : Nat) ->
122− so (offset + size <= i) ->
122+ So (offset + size <= i) ->
123123 { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)
124124peek offset size prf = call $ Peek offset size prf
125125
@@ -127,7 +127,7 @@ poke : {n : Nat} ->
127127 {i : Nat} ->
128128 (offset : Nat) ->
129129 Vect size Bits8 ->
130− so (offset <= i && offset + size <= n) ->
130+ So (offset <= i && offset + size <= n) ->
131131 Eff () [RAW_MEMORY (MemoryChunk n i)]
132132 (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])
133133poke offset content prf = call $ Poke offset content prf
@@ -144,8 +144,8 @@ move' : {dst_size : Nat} ->
144144 (dst_offset : Nat) ->
145145 (src_offset : Nat) ->
146146 (size : Nat) ->
147− so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
148− so (src_offset + size <= src_init) ->
147+ So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
148+ So (src_offset + size <= src_init) ->
149149 Eff () [RAW_MEMORY (MemoryChunk dst_size dst_init)]
150150 (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))])
151151move' src_ptr dst_offset src_offset size dst_bounds src_bounds
@@ -160,8 +160,8 @@ move : {dst_size : Nat} ->
160160 (dst_offset : Nat) ->
161161 (src_offset : Nat) ->
162162 (size : Nat) ->
163− so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
164− so (src_offset + size <= src_init) ->
163+ So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
164+ So (src_offset + size <= src_init) ->
165165 Eff ()
166166 [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)
167167 , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]
libs/prelude/Builtins.idr+20−4
@@ -3,11 +3,27 @@
33%access public
44%default total
55
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+
622||| Dependent pairs, in their internal representation
723||| @ a the type of the witness
824||| @ P the type of the proof
925data 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
1127
1228||| The eliminator for the empty type.
1329FalseElim : _|_ -> a
@@ -32,15 +48,15 @@ infix 5 ~=~
3248|||
3349||| This is used by the `rewrite` tactic and term.
3450replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
35−replace refl prf = prf
51+replace Refl prf = prf
3652
3753||| Symmetry of propositional equality
3854sym : {l:a} -> {r:a} -> l = r -> r = l
39−sym refl = refl
55+sym Refl = Refl
4056
4157||| Transitivity of propositional equality
4258trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c
43−trans refl refl = refl
59+trans Refl Refl = Refl
4460
4561||| There are two types of laziness: that arising from lazy functions, and that
4662||| arising from codata. They differ in their totality condition.
libs/prelude/Decidable/Equality.idr+45−45
@@ -31,17 +31,17 @@ class DecEq t where
3131--------------------------------------------------------------------------------
3232
3333instance DecEq () where
34− decEq () () = Yes refl
34+ decEq () () = Yes Refl
3535
3636--------------------------------------------------------------------------------
3737-- Booleans
3838--------------------------------------------------------------------------------
3939total trueNotFalse : True = False -> _|_
40−trueNotFalse refl impossible
40+trueNotFalse Refl impossible
4141
4242instance DecEq Bool where
43− decEq True True = Yes refl
44− decEq False False = Yes refl
43+ decEq True True = Yes Refl
44+ decEq False False = Yes Refl
4545 decEq True False = No trueNotFalse
4646 decEq False True = No (negEqSym trueNotFalse)
4747
@@ -50,10 +50,10 @@ instance DecEq Bool where
5050--------------------------------------------------------------------------------
5151
5252total OnotS : Z = S n -> _|_
53−OnotS refl impossible
53+OnotS Refl impossible
5454
5555instance DecEq Nat where
56− decEq Z Z = Yes refl
56+ decEq Z Z = Yes Refl
5757 decEq Z (S _) = No OnotS
5858 decEq (S _) Z = No (negEqSym OnotS)
5959 decEq (S n) (S m) with (decEq n m)
@@ -65,10 +65,10 @@ instance DecEq Nat where
6565--------------------------------------------------------------------------------
6666
6767total nothingNotJust : {x : t} -> (Nothing {a = t} = Just x) -> _|_
68−nothingNotJust refl impossible
68+nothingNotJust Refl impossible
6969
7070instance (DecEq t) => DecEq (Maybe t) where
71− decEq Nothing Nothing = Yes refl
71+ decEq Nothing Nothing = Yes Refl
7272 decEq (Just x') (Just y') with (decEq x' y')
7373 | Yes p = Yes $ cong p
7474 | No p = No $ \h : Just x' = Just y' => p $ justInjective h
@@ -80,7 +80,7 @@ instance (DecEq t) => DecEq (Maybe t) where
8080--------------------------------------------------------------------------------
8181
8282total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> _|_
83−leftNotRight refl impossible
83+leftNotRight Refl impossible
8484
8585instance (DecEq a, DecEq b) => DecEq (Either a b) where
8686 decEq (Left x') (Left y') with (decEq x' y')
@@ -96,40 +96,40 @@ instance (DecEq a, DecEq b) => DecEq (Either a b) where
9696-- Fin
9797--------------------------------------------------------------------------------
9898
99−total fZNotfS : {f : Fin n} -> fZ {k = n} = fS f -> _|_
100−fZNotfS refl impossible
99+total FZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> _|_
100+FZNotFS Refl impossible
101101
102102instance DecEq (Fin n) where
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')
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')
107107 | 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
109109
110110--------------------------------------------------------------------------------
111111-- Tuple
112112--------------------------------------------------------------------------------
113113
114114lemma_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
116116
117117lemma_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
119119
120120lemma_fst_neq_snd_eq : {x : a, x' : b, y : c, y' : d} ->
121121 (x = x' -> _|_) ->
122122 (y = y') ->
123123 ((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
125125
126126instance (DecEq a, DecEq b) => DecEq (a, b) where
127127 decEq (a, b) (a', b') with (decEq a a')
128− decEq (a, b) (a, b') | (Yes refl) with (decEq b b')
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)
128+ decEq (a, b) (a, b') | (Yes Refl) with (decEq b b')
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)
131131 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)
133133 decEq (a, b) (a', b') | (No p) | (No p') = No (\eq => lemma_both_neq p p' eq)
134134
135135
@@ -138,27 +138,27 @@ instance (DecEq a, DecEq b) => DecEq (a, b) where
138138--------------------------------------------------------------------------------
139139
140140lemma_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
142142
143143lemma_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
145145
146146lemma_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
148148
149149lemma_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
151151
152152instance DecEq a => DecEq (List a) where
153− decEq [] [] = Yes refl
153+ decEq [] [] = Yes Refl
154154 decEq (x :: xs) [] = No lemma_val_not_nil
155155 decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil)
156156 decEq (x :: xs) (y :: ys) with (decEq x y)
157− decEq (x :: xs) (x :: ys) | Yes refl with (decEq xs ys)
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)
157+ decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)
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)
160160 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)
162162 decEq (x :: xs) (y :: ys) | (No p) | (No p') = No (\eq => lemma_x_neq_xs_neq p p' eq)
163163
164164
@@ -168,26 +168,26 @@ instance DecEq a => DecEq (List a) where
168168
169169total
170170vectInjective1 : {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
172172
173173total
174174vectInjective2 : {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
176176
177177instance DecEq a => DecEq (Vect n a) where
178− decEq [] [] = Yes refl
178+ decEq [] [] = Yes Refl
179179 decEq (x :: xs) (y :: ys) with (decEq x y)
180− decEq (x :: xs) (x :: ys) | Yes refl with (decEq xs ys)
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)
180+ decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)
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)
183183 decEq (x :: xs) (y :: ys) | No neq = No (neq . vectInjective1)
184184
185185{- The following definition is elaborated in a wrong case-tree. Examination pending.
186186
187187instance DecEq a => DecEq (Vect n a) where
188− decEq [] [] = Yes refl
188+ decEq [] [] = Yes Refl
189189 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
191191 decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))
192192 decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))
193193-}
@@ -202,7 +202,7 @@ instance DecEq a => DecEq (Vect n a) where
202202instance DecEq Int where
203203 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
204204 where primitiveEq : x = y
205− primitiveEq = believe_me (refl {x})
205+ primitiveEq = believe_me (Refl {x})
206206 postulate primitiveNotEq : x = y -> _|_
207207
208208--------------------------------------------------------------------------------
@@ -212,7 +212,7 @@ instance DecEq Int where
212212instance DecEq Char where
213213 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
214214 where primitiveEq : x = y
215− primitiveEq = believe_me (refl {x})
215+ primitiveEq = believe_me (Refl {x})
216216 postulate primitiveNotEq : x = y -> _|_
217217
218218--------------------------------------------------------------------------------
@@ -222,7 +222,7 @@ instance DecEq Char where
222222instance DecEq Integer where
223223 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
224224 where primitiveEq : x = y
225− primitiveEq = believe_me (refl {x})
225+ primitiveEq = believe_me (Refl {x})
226226 postulate primitiveNotEq : x = y -> _|_
227227
228228--------------------------------------------------------------------------------
@@ -232,7 +232,7 @@ instance DecEq Integer where
232232instance DecEq Float where
233233 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
234234 where primitiveEq : x = y
235− primitiveEq = believe_me (refl {x})
235+ primitiveEq = believe_me (Refl {x})
236236 postulate primitiveNotEq : x = y -> _|_
237237
238238--------------------------------------------------------------------------------
@@ -242,7 +242,7 @@ instance DecEq Float where
242242instance DecEq String where
243243 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
244244 where primitiveEq : x = y
245− primitiveEq = believe_me (refl {x})
245+ primitiveEq = believe_me (Refl {x})
246246 postulate primitiveNotEq : x = y -> _|_
247247
248248
libs/prelude/Prelude.idr+3−3
@@ -420,9 +420,9 @@ instance Enum Int where
420420 go (x :: xs) = n + (cast x * inc) :: go xs
421421
422422instance Enum (Fin (S n)) where
423− pred fZ = fZ
424− pred (fS n) = weaken n
425− succ n = case strengthen (fS n) of
423+ pred FZ = FZ
424+ pred (FS n) = weaken n
425+ succ n = case strengthen (FS n) of
426426 Left _ => last
427427 Right k => k
428428 toNat n = cast n
libs/prelude/Prelude/Basics.idr+3−1
@@ -1,5 +1,7 @@
11module Prelude.Basics
22
3+import Builtins
4+
35Not : Type -> Type
46Not a = a -> _|_
57
@@ -42,7 +44,7 @@ apply f a = f a
4244
4345||| Equality is a congruence.
4446cong : {f : t -> u} -> (a = b) -> f a = f b
45−cong refl = refl
47+cong Refl = Refl
4648
4749||| Decidability. A decidable property either holds or is a contradiction.
4850data Dec : Type -> Type where
libs/prelude/Prelude/Bool.idr+4−3
@@ -24,10 +24,11 @@ boolElim False t e = e
2424||| If you find yourself using `so` for something other than primitive types,
2525||| it may be appropriate to define a type of evidence for the property that you
2626||| care about instead.
27−data so : Bool -> Type where oh : so True
27+data So : Bool -> Type where
28+ Oh : So True
2829
29−instance Uninhabited (so False) where
30− uninhabited oh impossible
30+instance Uninhabited (So False) where
31+ uninhabited Oh impossible
3132
3233-- Syntactic sugar for boolean elimination.
3334syntax 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
3030-- Misc.
3131--------------------------------------------------------------------------------
3232
33−||| Perform a case analysis on a Boolean, providing clients with a `so` proof
34−choose : (b : Bool) -> Either (so b) (so (not b))
35−choose True = Left oh
36−choose False = Right oh
33+||| Perform a case analysis on a Boolean, providing clients with a `So` proof
34+choose : (b : Bool) -> Either (So b) (So (not b))
35+choose True = Left Oh
36+choose False = Right Oh
3737
3838||| Simply-typed eliminator for Either
3939||| @ f the action to take on Left
@@ -97,9 +97,9 @@ instance (Eq a, Eq b) => Eq (Either a b) where
9797||| Left is injective
9898total leftInjective : {b : Type} -> {x : a} -> {y : a}
9999 -> (Left {b = b} x = Left {b = b} y) -> (x = y)
100−leftInjective refl = refl
100+leftInjective Refl = Refl
101101
102102||| Right is injective
103103total rightInjective : {a : Type} -> {x : b} -> {y : b}
104104 -> (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
1212||| exceedingly inefficient at run time.
1313||| @ n the upper bound
1414data Fin : (n : Nat) -> Type where
15− fZ : Fin (S k)
16− fS : Fin k -> Fin (S k)
15+ FZ : Fin (S k)
16+ FS : Fin k -> Fin (S k)
1717
1818instance Uninhabited (Fin Z) where
19− uninhabited fZ impossible
20− uninhabited (fS f) impossible
19+ uninhabited FZ impossible
20+ uninhabited (FS f) impossible
2121
22−fSInjective : (m : Fin k) -> (n : Fin k) -> fS m = fS n -> m = n
23−fSInjective left _ refl = refl
22+FSInjective : (m : Fin k) -> (n : Fin k) -> FS m = FS n -> m = n
23+FSInjective left _ Refl = Refl
2424
2525instance Eq (Fin n) where
26− (==) fZ fZ = True
27− (==) (fS k) (fS k') = k == k'
26+ (==) FZ FZ = True
27+ (==) (FS k) (FS k') = k == k'
2828 (==) _ _ = False
2929
3030||| There are no elements of `Fin Z`
3131FinZAbsurd : Fin Z -> _|_
32−FinZAbsurd fZ impossible
32+FinZAbsurd FZ impossible
3333
3434FinZElim : Fin Z -> a
3535FinZElim x = FalseElim (FinZAbsurd x)
3636
3737||| Convert a Fin to a Nat
3838finToNat : Fin n -> Nat
39−finToNat fZ = Z
40−finToNat (fS k) = S (finToNat k)
39+finToNat FZ = Z
40+finToNat (FS k) = S (finToNat k)
4141
4242||| `finToNat` is injective
4343finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
44−finToNatInjective fZ fZ refl = refl
45−finToNatInjective (fS m) fZ refl impossible
46−finToNatInjective fZ (fS n) refl impossible
47−finToNatInjective (fS m) (fS n) prf =
44+finToNatInjective FZ FZ Refl = Refl
45+finToNatInjective (FS m) FZ Refl impossible
46+finToNatInjective FZ (FS n) Refl impossible
47+finToNatInjective (FS m) (FS n) prf =
4848 cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))
4949
5050instance Cast (Fin n) Nat where
@@ -52,29 +52,29 @@ instance Cast (Fin n) Nat where
5252
5353||| Convert a Fin to an Integer
5454finToInteger : Fin n -> Integer
55−finToInteger fZ = 0
56−finToInteger (fS k) = 1 + finToInteger k
55+finToInteger FZ = 0
56+finToInteger (FS k) = 1 + finToInteger k
5757
5858instance Cast (Fin n) Integer where
5959 cast x = finToInteger x
6060
6161||| Weaken the bound on a Fin by 1
6262weaken : Fin n -> Fin (S n)
63−weaken fZ = fZ
64−weaken (fS k) = fS (weaken k)
63+weaken FZ = FZ
64+weaken (FS k) = FS (weaken k)
6565
6666||| Weaken the bound on a Fin by some amount
6767weakenN : (n : Nat) -> Fin m -> Fin (m + n)
68−weakenN n fZ = fZ
69−weakenN n (fS f) = fS (weakenN n f)
68+weakenN n FZ = FZ
69+weakenN n (FS f) = FS (weakenN n f)
7070
7171||| Attempt to tighten the bound on a Fin.
7272||| Return `Left` if the bound could not be tightened, or `Right` if it could.
7373strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
74−strengthen {n = S k} fZ = Right fZ
75−strengthen {n = S k} (fS i) with (strengthen i)
76− strengthen (fS k) | Left x = Left (fS x)
77− strengthen (fS k) | Right x = Right (fS x)
74+strengthen {n = S k} FZ = Right FZ
75+strengthen {n = S k} (FS i) with (strengthen i)
76+ strengthen (FS k) | Left x = Left (FS x)
77+ strengthen (FS k) | Right x = Right (FS x)
7878strengthen f = Left f
7979
8080||| Add some natural number to a Fin, extending the bound accordingly
@@ -82,24 +82,24 @@ strengthen f = Left f
8282||| @ m the number to increase the Fin by
8383shift : (m : Nat) -> Fin n -> Fin (m + n)
8484shift 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)
8686
8787||| The largest element of some Fin type
8888last : Fin (S n)
89−last {n=Z} = fZ
90−last {n=S _} = fS last
89+last {n=Z} = FZ
90+last {n=S _} = FS last
9191
92−total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
93−fSinjective refl = refl
92+total FSinjective : {f : Fin n} -> {f' : Fin n} -> (FS f = FS f') -> f = f'
93+FSinjective Refl = Refl
9494
9595instance Ord (Fin n) where
96− compare fZ fZ = EQ
97− compare fZ (fS _) = LT
98− compare (fS _) fZ = GT
99− compare (fS x) (fS y) = compare x y
96+ compare FZ FZ = EQ
97+ compare FZ (FS _) = LT
98+ compare (FS _) FZ = GT
99+ compare (FS x) (FS y) = compare x y
100100
101101instance MinBound (Fin (S n)) where
102− minBound = fZ
102+ minBound = FZ
103103
104104instance MaxBound (Fin (S n)) where
105105 maxBound = last
@@ -107,28 +107,28 @@ instance MaxBound (Fin (S n)) where
107107
108108||| Add two Fins, extending the bound
109109(+) : Fin n -> Fin m -> Fin (n + m)
110−(+) {n=S n} {m=m} fZ f' = rewrite plusCommutative n m in weaken (weakenN n f')
111−(+) (fS f) f' = fS (f + 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')
112112
113113||| Substract two Fins, keeping the bound of the minuend
114114(-) : Fin n -> Fin m -> Fin n
115−fZ - _ = fZ
116−f - fZ = f
117−(fS f) - (fS f') = weaken $ f - f'
115+FZ - _ = FZ
116+f - FZ = f
117+(FS f) - (FS f') = weaken $ f - f'
118118
119119||| Multiply two Fins, extending the bound
120120(*) : Fin n -> Fin m -> Fin (n * m)
121121(*) {n=Z} f f' = FinZElim f
122122(*) {m=Z} f f' = FinZElim f'
123−(*) {n=S n} {m=S m} fZ f' = fZ
124−(*) {n=S n} {m=S m} (fS f) f' = f' + (f * f')
123+(*) {n=S n} {m=S m} FZ f' = FZ
124+(*) {n=S n} {m=S m} (FS f) f' = f' + (f * f')
125125
126126-- Construct a Fin from an integer literal which must fit in the given Fin
127127
128128natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
129−natToFin Z (S j) = Just fZ
129+natToFin Z (S j) = Just FZ
130130natToFin (S k) (S j) with (natToFin k j)
131− | Just k' = Just (fS k')
131+ | Just k' = Just (FS k')
132132 | Nothing = Nothing
133133natToFin _ _ = Nothing
134134
libs/prelude/Prelude/List.idr+20−20
@@ -60,7 +60,7 @@ length (x::xs) = 1 + length xs
6060index : (n : Nat) -> (l : List a) -> (ok : lt n (length l) = True) -> a
6161index Z (x::xs) p = x
6262index (S n) (x::xs) p = index n xs ?indexTailProof
63−index _ [] refl impossible
63+index _ [] Refl impossible
6464
6565||| Attempt to find a particular element of a list.
6666|||
@@ -73,7 +73,7 @@ index' _ [] = Nothing
7373||| Get the first element of a non-empty list
7474||| @ ok proof that the list is non-empty
7575head : (l : List a) -> {auto ok : isCons l = True} -> a
76−head [] {ok=refl} impossible
76+head [] {ok=Refl} impossible
7777head (x::xs) {ok=p} = x
7878
7979||| Attempt to get the first element of a list. If the list is empty, return
@@ -85,7 +85,7 @@ head' (x::xs) = Just x
8585||| Get the tail of a non-empty list.
8686||| @ ok proof that the list is non-empty
8787tail : (l : List a) -> {auto ok : isCons l = True} -> List a
88−tail [] {ok=refl} impossible
88+tail [] {ok=Refl} impossible
8989tail (x::xs) {ok=p} = xs
9090
9191||| Attempt to get the tail of a list.
@@ -98,9 +98,9 @@ tail' (x::xs) = Just xs
9898||| Retrieve the last element of a non-empty list.
9999||| @ ok proof that the list is non-empty
100100last : (l : List a) -> {auto ok : isCons l = True} -> a
101−last [] {ok=refl} impossible
101+last [] {ok=Refl} impossible
102102last [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}
104104
105105||| Attempt to retrieve the last element of a non-empty list.
106106|||
@@ -115,9 +115,9 @@ last' (x::xs) =
115115||| Return all but the last element of a non-empty list.
116116||| @ ok proof that the list is non-empty
117117init : (l : List a) -> {auto ok : isCons l = True} -> List a
118−init [] {ok=refl} impossible
118+init [] {ok=Refl} impossible
119119init [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}
121121
122122||| Attempt to Return all but the last element of a list.
123123|||
@@ -251,8 +251,8 @@ instance Functor List where
251251||| @ ok a proof that the lengths of the inputs are equal
252252zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->
253253 (ok : length l = length r) -> List c
254−zipWith f [] (y::ys) refl impossible
255−zipWith f (x::xs) [] refl impossible
254+zipWith f [] (y::ys) Refl impossible
255+zipWith f (x::xs) [] Refl impossible
256256zipWith f [] [] p = []
257257zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)
258258
@@ -265,10 +265,10 @@ zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)
265265||| @ ok' a proof that the lengths of the second and third inputs are equal
266266zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->
267267 (z : List c) -> (ok : length x = length y) -> (ok' : length y = length z) -> List d
268−zipWith3 f _ [] (z::zs) p refl impossible
269−zipWith3 f _ (y::ys) [] p refl impossible
270−zipWith3 f [] (y::ys) _ refl q impossible
271−zipWith3 f (x::xs) [] _ refl q impossible
268+zipWith3 f _ [] (z::zs) p Refl impossible
269+zipWith3 f _ (y::ys) [] p Refl impossible
270+zipWith3 f [] (y::ys) _ Refl q impossible
271+zipWith3 f (x::xs) [] _ Refl q impossible
272272zipWith3 f [] [] [] p q = []
273273zipWith3 f (x::xs) (y::ys) (z::zs) p q =
274274 f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')
@@ -651,7 +651,7 @@ catMaybes (x::xs) =
651651||| The empty list is a right identity for append.
652652appendNilRightNeutral : (l : List a) ->
653653 l ++ [] = l
654−appendNilRightNeutral [] = refl
654+appendNilRightNeutral [] = Refl
655655appendNilRightNeutral (x::xs) =
656656 let inductiveHypothesis = appendNilRightNeutral xs in
657657 ?appendNilRightNeutralStepCase
@@ -659,7 +659,7 @@ appendNilRightNeutral (x::xs) =
659659||| Appending lists is associative.
660660appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->
661661 l ++ (c ++ r) = (l ++ c) ++ r
662−appendAssociative [] c r = refl
662+appendAssociative [] c r = Refl
663663appendAssociative (x::xs) c r =
664664 let inductiveHypothesis = appendAssociative xs c r in
665665 ?appendAssociativeStepCase
@@ -668,7 +668,7 @@ appendAssociative (x::xs) c r =
668668||| of the input lists.
669669lengthAppend : (left : List a) -> (right : List a) ->
670670 length (left ++ right) = length left + length right
671−lengthAppend [] right = refl
671+lengthAppend [] right = Refl
672672lengthAppend (x::xs) right =
673673 let inductiveHypothesis = lengthAppend xs right in
674674 ?lengthAppendStepCase
@@ -676,7 +676,7 @@ lengthAppend (x::xs) right =
676676||| Mapping a function over a list doesn't change its length.
677677mapPreservesLength : (f : a -> b) -> (l : List a) ->
678678 length (map f l) = length l
679−mapPreservesLength f [] = refl
679+mapPreservesLength f [] = Refl
680680mapPreservesLength f (x::xs) =
681681 let inductiveHypothesis = mapPreservesLength f xs in
682682 ?mapPreservesLengthStepCase
@@ -685,7 +685,7 @@ mapPreservesLength f (x::xs) =
685685||| to appending them and then mapping the function.
686686mapDistributesOverAppend : (f : a -> b) -> (l : List a) -> (r : List a) ->
687687 map f (l ++ r) = map f l ++ map f r
688−mapDistributesOverAppend f [] r = refl
688+mapDistributesOverAppend f [] r = Refl
689689mapDistributesOverAppend f (x::xs) r =
690690 let inductiveHypothesis = mapDistributesOverAppend f xs r in
691691 ?mapDistributesOverAppendStepCase
@@ -693,7 +693,7 @@ mapDistributesOverAppend f (x::xs) r =
693693||| Mapping two functions is the same as mapping their composition.
694694mapFusion : (f : b -> c) -> (g : a -> b) -> (l : List a) ->
695695 map f (map g l) = map (f . g) l
696−mapFusion f g [] = refl
696+mapFusion f g [] = Refl
697697mapFusion f g (x::xs) =
698698 let inductiveHypothesis = mapFusion f g xs in
699699 ?mapFusionStepCase
@@ -701,7 +701,7 @@ mapFusion f g (x::xs) =
701701||| No list contains an element of the empty list by any predicate.
702702hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->
703703 hasAnyBy p [] l = False
704−hasAnyByNilFalse p [] = refl
704+hasAnyByNilFalse p [] = Refl
705705hasAnyByNilFalse p (x::xs) =
706706 let inductiveHypothesis = hasAnyByNilFalse p xs in
707707 ?hasAnyByNilFalseStepCase
libs/prelude/Prelude/Maybe.idr+1−1
@@ -45,7 +45,7 @@ toMaybe True j = Just j
4545toMaybe False j = Nothing
4646
4747justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y
48−justInjective refl = refl
48+justInjective Refl = Refl
4949
5050||| Convert a `Maybe a` value to an `a` value, using `neutral` in the case
5151||| that the `Maybe` value is `Nothing`.
libs/prelude/Prelude/Nat.idr+107−107
@@ -22,7 +22,7 @@ import Prelude.Uninhabited
2222%name Nat k,j,i,n,m
2323
2424instance Uninhabited (Z = S n) where
25− uninhabited refl impossible
25+ uninhabited Refl impossible
2626
2727--------------------------------------------------------------------------------
2828-- Syntactic tests
@@ -94,9 +94,9 @@ hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)
9494||| @ m the larger number
9595data LTE : (n, m : Nat) -> Type where
9696 ||| Zero is the smallest Nat
97− lteZero : LTE Z right
97+ LTEZero : LTE Z right
9898 ||| 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)
100100
101101||| Greater than or equal to
102102total GTE : Nat -> Nat -> Type
@@ -112,18 +112,18 @@ GT left right = LT right left
112112
113113||| A successor is never less than or equal zero
114114succNotLTEzero : Not (S m `LTE` Z)
115−succNotLTEzero lteZero impossible
115+succNotLTEzero LTEZero impossible
116116
117117||| If two numbers are ordered, their predecessors are too
118118fromLteSucc : (S m `LTE` S n) -> (m `LTE` n)
119−fromLteSucc (lteSucc x) = x
119+fromLteSucc (LTESucc x) = x
120120
121121||| A decision procedure for `LTE`
122122isLTE : (m, n : Nat) -> Dec (m `LTE` n)
123−isLTE Z n = Yes lteZero
123+isLTE Z n = Yes LTEZero
124124isLTE (S k) Z = No succNotLTEzero
125125isLTE (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)
127127 isLTE (S k) (S j) | (No contra) = No (contra . fromLteSucc)
128128
129129||| 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)
329329-- An informative comparison view
330330--------------------------------------------------------------------------------
331331data CmpNat : Nat -> Nat -> Type where
332− cmpLT : (y : _) -> CmpNat x (x + S y)
333− cmpEQ : CmpNat x x
334− cmpGT : (x : _) -> CmpNat (y + S x) y
332+ CmpLT : (y : _) -> CmpNat x (x + S y)
333+ CmpEQ : CmpNat x x
334+ CmpGT : (x : _) -> CmpNat (y + S x) y
335335
336336total cmp : (x, y : Nat) -> CmpNat x y
337−cmp Z Z = cmpEQ
338−cmp Z (S k) = cmpLT _
339−cmp (S k) Z = cmpGT _
337+cmp Z Z = CmpEQ
338+cmp Z (S k) = CmpLT _
339+cmp (S k) Z = CmpGT _
340340cmp (S x) (S y) with (cmp x y)
341− cmp (S x) (S (x + (S k))) | cmpLT k = cmpLT k
342− cmp (S x) (S x) | cmpEQ = cmpEQ
343− cmp (S (y + (S k))) (S y) | cmpGT k = cmpGT k
341+ cmp (S x) (S (x + (S k))) | CmpLT k = CmpLT k
342+ cmp (S x) (S x) | CmpEQ = CmpEQ
343+ cmp (S (y + (S k))) (S y) | CmpGT k = CmpGT k
344344
345345--------------------------------------------------------------------------------
346346-- Properties
@@ -351,26 +351,26 @@ cmp (S x) (S y) with (cmp x y)
351351||| S preserves equality
352352total eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->
353353 S left = S right
354−eqSucc left _ refl = refl
354+eqSucc left _ Refl = Refl
355355
356356||| S is injective
357357total succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
358358 left = right
359−succInjective left _ refl = refl
359+succInjective left _ Refl = Refl
360360
361361-- Plus
362362total plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
363−plusZeroLeftNeutral right = refl
363+plusZeroLeftNeutral right = Refl
364364
365365total plusZeroRightNeutral : (left : Nat) -> left + 0 = left
366−plusZeroRightNeutral Z = refl
366+plusZeroRightNeutral Z = Refl
367367plusZeroRightNeutral (S n) =
368368 let inductiveHypothesis = plusZeroRightNeutral n in
369369 ?plusZeroRightNeutralStepCase
370370
371371total plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
372372 S (left + right) = left + (S right)
373−plusSuccRightSucc Z right = refl
373+plusSuccRightSucc Z right = Refl
374374plusSuccRightSucc (S left) right =
375375 let inductiveHypothesis = plusSuccRightSucc left right in
376376 ?plusSuccRightSuccStepCase
@@ -384,21 +384,21 @@ plusCommutative (S left) right =
384384
385385total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
386386 left + (centre + right) = (left + centre) + right
387−plusAssociative Z centre right = refl
387+plusAssociative Z centre right = Refl
388388plusAssociative (S left) centre right =
389389 let inductiveHypothesis = plusAssociative left centre right in
390390 ?plusAssociativeStepCase
391391
392392total plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
393393 (p : left = right) -> left + c = right + c
394−plusConstantRight left _ c refl = refl
394+plusConstantRight left _ c Refl = Refl
395395
396396total plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
397397 (p : left = right) -> c + left = c + right
398−plusConstantLeft left _ c refl = refl
398+plusConstantLeft left _ c Refl = Refl
399399
400400total plusOneSucc : (right : Nat) -> 1 + right = S right
401−plusOneSucc n = refl
401+plusOneSucc n = Refl
402402
403403total plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
404404 (p : left + right = left + right') -> right = right'
@@ -423,24 +423,24 @@ plusLeftLeftRightZero (S left) right p =
423423
424424-- Mult
425425total multZeroLeftZero : (right : Nat) -> Z * right = Z
426−multZeroLeftZero right = refl
426+multZeroLeftZero right = Refl
427427
428428total multZeroRightZero : (left : Nat) -> left * Z = Z
429−multZeroRightZero Z = refl
429+multZeroRightZero Z = Refl
430430multZeroRightZero (S left) =
431431 let inductiveHypothesis = multZeroRightZero left in
432432 ?multZeroRightZeroStepCase
433433
434434total multRightSuccPlus : (left : Nat) -> (right : Nat) ->
435435 left * (S right) = left + (left * right)
436−multRightSuccPlus Z right = refl
436+multRightSuccPlus Z right = Refl
437437multRightSuccPlus (S left) right =
438438 let inductiveHypothesis = multRightSuccPlus left right in
439439 ?multRightSuccPlusStepCase
440440
441441total multLeftSuccPlus : (left : Nat) -> (right : Nat) ->
442442 (S left) * right = right + (left * right)
443−multLeftSuccPlus left right = refl
443+multLeftSuccPlus left right = Refl
444444
445445total multCommutative : (left : Nat) -> (right : Nat) ->
446446 left * right = right * left
@@ -451,33 +451,33 @@ multCommutative (S left) right =
451451
452452total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
453453 left * (centre + right) = (left * centre) + (left * right)
454−multDistributesOverPlusRight Z centre right = refl
454+multDistributesOverPlusRight Z centre right = Refl
455455multDistributesOverPlusRight (S left) centre right =
456456 let inductiveHypothesis = multDistributesOverPlusRight left centre right in
457457 ?multDistributesOverPlusRightStepCase
458458
459459total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
460460 (left + centre) * right = (left * right) + (centre * right)
461−multDistributesOverPlusLeft Z centre right = refl
461+multDistributesOverPlusLeft Z centre right = Refl
462462multDistributesOverPlusLeft (S left) centre right =
463463 let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
464464 ?multDistributesOverPlusLeftStepCase
465465
466466total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
467467 left * (centre * right) = (left * centre) * right
468−multAssociative Z centre right = refl
468+multAssociative Z centre right = Refl
469469multAssociative (S left) centre right =
470470 let inductiveHypothesis = multAssociative left centre right in
471471 ?multAssociativeStepCase
472472
473473total multOneLeftNeutral : (right : Nat) -> 1 * right = right
474−multOneLeftNeutral Z = refl
474+multOneLeftNeutral Z = Refl
475475multOneLeftNeutral (S right) =
476476 let inductiveHypothesis = multOneLeftNeutral right in
477477 ?multOneLeftNeutralStepCase
478478
479479total multOneRightNeutral : (left : Nat) -> left * 1 = left
480−multOneRightNeutral Z = refl
480+multOneRightNeutral Z = Refl
481481multOneRightNeutral (S left) =
482482 let inductiveHypothesis = multOneRightNeutral left in
483483 ?multOneRightNeutralStepCase
@@ -485,53 +485,53 @@ multOneRightNeutral (S left) =
485485-- Minus
486486total minusSuccSucc : (left : Nat) -> (right : Nat) ->
487487 (S left) - (S right) = left - right
488−minusSuccSucc left right = refl
488+minusSuccSucc left right = Refl
489489
490490total minusZeroLeft : (right : Nat) -> 0 - right = Z
491−minusZeroLeft right = refl
491+minusZeroLeft right = Refl
492492
493493total minusZeroRight : (left : Nat) -> left - 0 = left
494−minusZeroRight Z = refl
495−minusZeroRight (S left) = refl
494+minusZeroRight Z = Refl
495+minusZeroRight (S left) = Refl
496496
497497total minusZeroN : (n : Nat) -> Z = n - n
498−minusZeroN Z = refl
498+minusZeroN Z = Refl
499499minusZeroN (S n) = minusZeroN n
500500
501501total minusOneSuccN : (n : Nat) -> S Z = (S n) - n
502−minusOneSuccN Z = refl
502+minusOneSuccN Z = Refl
503503minusOneSuccN (S n) = minusOneSuccN n
504504
505505total minusSuccOne : (n : Nat) -> S n - 1 = n
506−minusSuccOne Z = refl
507−minusSuccOne (S n) = refl
506+minusSuccOne Z = Refl
507+minusSuccOne (S n) = Refl
508508
509509total minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = Z
510−minusPlusZero Z m = refl
510+minusPlusZero Z m = Refl
511511minusPlusZero (S n) m = minusPlusZero n m
512512
513513total minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
514514 left - centre - right = left - (centre + right)
515−minusMinusMinusPlus Z Z right = refl
516−minusMinusMinusPlus (S left) Z right = refl
517−minusMinusMinusPlus Z (S centre) right = refl
515+minusMinusMinusPlus Z Z right = Refl
516+minusMinusMinusPlus (S left) Z right = Refl
517+minusMinusMinusPlus Z (S centre) right = Refl
518518minusMinusMinusPlus (S left) (S centre) right =
519519 let inductiveHypothesis = minusMinusMinusPlus left centre right in
520520 ?minusMinusMinusPlusStepCase
521521
522522total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
523523 (left + right) - (left + right') = right - right'
524−plusMinusLeftCancel Z right right' = refl
524+plusMinusLeftCancel Z right right' = Refl
525525plusMinusLeftCancel (S left) right right' =
526526 let inductiveHypothesis = plusMinusLeftCancel left right right' in
527527 ?plusMinusLeftCancelStepCase
528528
529529total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
530530 (left - centre) * right = (left * right) - (centre * right)
531−multDistributesOverMinusLeft Z Z right = refl
531+multDistributesOverMinusLeft Z Z right = Refl
532532multDistributesOverMinusLeft (S left) Z right =
533533 ?multDistributesOverMinusLeftBaseCase
534−multDistributesOverMinusLeft Z (S centre) right = refl
534+multDistributesOverMinusLeft Z (S centre) right = Refl
535535multDistributesOverMinusLeft (S left) (S centre) right =
536536 let inductiveHypothesis = multDistributesOverMinusLeft left centre right in
537537 ?multDistributesOverMinusLeftStepCase
@@ -544,7 +544,7 @@ multDistributesOverMinusRight left centre right =
544544-- Power
545545total powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
546546 base * (power base exp)
547−powerSuccPowerLeft base exp = refl
547+powerSuccPowerLeft base exp = Refl
548548
549549total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
550550 (power base exp) * (power base exp') = power base (exp + exp')
@@ -554,22 +554,22 @@ multPowerPowerPlus base (S exp) exp' =
554554 ?multPowerPowerPlusStepCase
555555
556556total powerZeroOne : (base : Nat) -> power base 0 = S Z
557−powerZeroOne base = refl
557+powerZeroOne base = Refl
558558
559559total powerOneNeutral : (base : Nat) -> power base 1 = base
560−powerOneNeutral Z = refl
560+powerOneNeutral Z = Refl
561561powerOneNeutral (S base) =
562562 let inductiveHypothesis = powerOneNeutral base in
563563 ?powerOneNeutralStepCase
564564
565565total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z
566−powerOneSuccOne Z = refl
566+powerOneSuccOne Z = Refl
567567powerOneSuccOne (S exp) =
568568 let inductiveHypothesis = powerOneSuccOne exp in
569569 ?powerOneSuccOneStepCase
570570
571571total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
572−powerSuccSuccMult Z = refl
572+powerSuccSuccMult Z = Refl
573573powerSuccSuccMult (S base) =
574574 let inductiveHypothesis = powerSuccSuccMult base in
575575 ?powerSuccSuccMultStepCase
@@ -583,11 +583,11 @@ powerPowerMultPower base exp (S exp') =
583583
584584-- Pred
585585total predSucc : (n : Nat) -> pred (S n) = n
586−predSucc n = refl
586+predSucc n = Refl
587587
588588total minusSuccPred : (left : Nat) -> (right : Nat) ->
589589 left - (S right) = pred (left - right)
590−minusSuccPred Z right = refl
590+minusSuccPred Z right = Refl
591591minusSuccPred (S left) Z =
592592 let inductiveHypothesis = minusSuccPred left Z in
593593 ?minusSuccPredStepCase
@@ -598,125 +598,125 @@ minusSuccPred (S left) (S right) =
598598-- boolElim
599599total boolElimSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->
600600 S (boolElim cond t f) = boolElim cond (S t) (S f)
601−boolElimSuccSucc True t f = refl
602−boolElimSuccSucc False t f = refl
601+boolElimSuccSucc True t f = Refl
602+boolElimSuccSucc False t f = Refl
603603
604604total boolElimPlusPlusLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
605605 left + (boolElim cond t f) = boolElim cond (left + t) (left + f)
606−boolElimPlusPlusLeft True left t f = refl
607−boolElimPlusPlusLeft False left t f = refl
606+boolElimPlusPlusLeft True left t f = Refl
607+boolElimPlusPlusLeft False left t f = Refl
608608
609609total boolElimPlusPlusRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
610610 (boolElim cond t f) + right = boolElim cond (t + right) (f + right)
611−boolElimPlusPlusRight True right t f = refl
612−boolElimPlusPlusRight False right t f = refl
611+boolElimPlusPlusRight True right t f = Refl
612+boolElimPlusPlusRight False right t f = Refl
613613
614614total boolElimMultMultLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
615615 left * (boolElim cond t f) = boolElim cond (left * t) (left * f)
616−boolElimMultMultLeft True left t f = refl
617−boolElimMultMultLeft False left t f = refl
616+boolElimMultMultLeft True left t f = Refl
617+boolElimMultMultLeft False left t f = Refl
618618
619619total boolElimMultMultRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
620620 (boolElim cond t f) * right = boolElim cond (t * right) (f * right)
621−boolElimMultMultRight True right t f = refl
622−boolElimMultMultRight False right t f = refl
621+boolElimMultMultRight True right t f = Refl
622+boolElimMultMultRight False right t f = Refl
623623
624624-- Orders
625625total lteNTrue : (n : Nat) -> lte n n = True
626−lteNTrue Z = refl
626+lteNTrue Z = Refl
627627lteNTrue (S n) = lteNTrue n
628628
629−total lteSuccZeroFalse : (n : Nat) -> lte (S n) Z = False
630−lteSuccZeroFalse Z = refl
631−lteSuccZeroFalse (S n) = refl
629+total LTESuccZeroFalse : (n : Nat) -> lte (S n) Z = False
630+LTESuccZeroFalse Z = Refl
631+LTESuccZeroFalse (S n) = Refl
632632
633633-- Minimum and maximum
634634total maximumAssociative : (l,c,r : Nat) -> maximum l (maximum c r) = maximum (maximum l c) r
635−maximumAssociative Z c r = refl
636−maximumAssociative (S k) Z r = refl
637−maximumAssociative (S k) (S j) Z = refl
638−maximumAssociative (S k) (S j) (S i) = rewrite maximumAssociative k j i in refl
635+maximumAssociative Z c r = Refl
636+maximumAssociative (S k) Z r = Refl
637+maximumAssociative (S k) (S j) Z = Refl
638+maximumAssociative (S k) (S j) (S i) = rewrite maximumAssociative k j i in Refl
639639
640640total maximumCommutative : (l, r : Nat) -> maximum l r = maximum r l
641−maximumCommutative Z Z = refl
642−maximumCommutative Z (S k) = refl
643−maximumCommutative (S k) Z = refl
644−maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in refl
641+maximumCommutative Z Z = Refl
642+maximumCommutative Z (S k) = Refl
643+maximumCommutative (S k) Z = Refl
644+maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in Refl
645645
646646total maximumIdempotent : (n : Nat) -> maximum n n = n
647−maximumIdempotent Z = refl
647+maximumIdempotent Z = Refl
648648maximumIdempotent (S k) = cong (maximumIdempotent k)
649649
650650total minimumAssociative : (l,c,r : Nat) -> minimum l (minimum c r) = minimum (minimum l c) r
651−minimumAssociative Z c r = refl
652−minimumAssociative (S k) Z r = refl
653−minimumAssociative (S k) (S j) Z = refl
654−minimumAssociative (S k) (S j) (S i) = rewrite minimumAssociative k j i in refl
651+minimumAssociative Z c r = Refl
652+minimumAssociative (S k) Z r = Refl
653+minimumAssociative (S k) (S j) Z = Refl
654+minimumAssociative (S k) (S j) (S i) = rewrite minimumAssociative k j i in Refl
655655
656656total minimumCommutative : (l, r : Nat) -> minimum l r = minimum r l
657−minimumCommutative Z Z = refl
658−minimumCommutative Z (S k) = refl
659−minimumCommutative (S k) Z = refl
660−minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in refl
657+minimumCommutative Z Z = Refl
658+minimumCommutative Z (S k) = Refl
659+minimumCommutative (S k) Z = Refl
660+minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in Refl
661661
662662total minimumIdempotent : (n : Nat) -> minimum n n = n
663−minimumIdempotent Z = refl
663+minimumIdempotent Z = Refl
664664minimumIdempotent (S k) = cong (minimumIdempotent k)
665665
666666total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z
667−minimumZeroZeroRight Z = refl
667+minimumZeroZeroRight Z = Refl
668668minimumZeroZeroRight (S right) = minimumZeroZeroRight right
669669
670670total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
671−minimumZeroZeroLeft Z = refl
672−minimumZeroZeroLeft (S left) = refl
671+minimumZeroZeroLeft Z = Refl
672+minimumZeroZeroLeft (S left) = Refl
673673
674674total minimumSuccSucc : (left : Nat) -> (right : Nat) ->
675675 minimum (S left) (S right) = S (minimum left right)
676−minimumSuccSucc Z Z = refl
677−minimumSuccSucc (S left) Z = refl
678−minimumSuccSucc Z (S right) = refl
676+minimumSuccSucc Z Z = Refl
677+minimumSuccSucc (S left) Z = Refl
678+minimumSuccSucc Z (S right) = Refl
679679minimumSuccSucc (S left) (S right) =
680680 let inductiveHypothesis = minimumSuccSucc left right in
681681 ?minimumSuccSuccStepCase
682682
683683total maximumZeroNRight : (right : Nat) -> maximum Z right = right
684−maximumZeroNRight Z = refl
685−maximumZeroNRight (S right) = refl
684+maximumZeroNRight Z = Refl
685+maximumZeroNRight (S right) = Refl
686686
687687total maximumZeroNLeft : (left : Nat) -> maximum left Z = left
688−maximumZeroNLeft Z = refl
689−maximumZeroNLeft (S left) = refl
688+maximumZeroNLeft Z = Refl
689+maximumZeroNLeft (S left) = Refl
690690
691691total maximumSuccSucc : (left : Nat) -> (right : Nat) ->
692692 S (maximum left right) = maximum (S left) (S right)
693−maximumSuccSucc Z Z = refl
694−maximumSuccSucc (S left) Z = refl
695−maximumSuccSucc Z (S right) = refl
693+maximumSuccSucc Z Z = Refl
694+maximumSuccSucc (S left) Z = Refl
695+maximumSuccSucc Z (S right) = Refl
696696maximumSuccSucc (S left) (S right) =
697697 let inductiveHypothesis = maximumSuccSucc left right in
698698 ?maximumSuccSuccStepCase
699699
700700total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
701−sucMaxL Z = refl
701+sucMaxL Z = Refl
702702sucMaxL (S l) = cong (sucMaxL l)
703703
704704total sucMaxR : (l : Nat) -> maximum l (S l) = (S l)
705−sucMaxR Z = refl
705+sucMaxR Z = Refl
706706sucMaxR (S l) = cong (sucMaxR l)
707707
708708total sucMinL : (l : Nat) -> minimum (S l) l = l
709−sucMinL Z = refl
709+sucMinL Z = Refl
710710sucMinL (S l) = cong (sucMinL l)
711711
712712total sucMinR : (l : Nat) -> minimum l (S l) = l
713−sucMinR Z = refl
713+sucMinR Z = Refl
714714sucMinR (S l) = cong (sucMinR l)
715715
716716-- div and mod
717717total modZeroZero : (n : Nat) -> mod 0 n = Z
718−modZeroZero Z = refl
719−modZeroZero (S n) = refl
718+modZeroZero Z = Refl
719+modZeroZero (S n) = Refl
720720
721721--------------------------------------------------------------------------------
722722-- Proofs
libs/prelude/Prelude/Pairs.idr+6−6
@@ -9,27 +9,27 @@ using (a : Type, P : a -> Type)
99
1010 ||| Dependent pair where the first field is erased.
1111 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
1313
1414 ||| Dependent pair where the second field is erased.
1515 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
1717
1818 -- Monomorphic projections
1919
2020 namespace Exists
2121 getWitness : Exists {a} P -> a
22− getWitness (evidence x pf) = x
22+ getWitness (Evidence x pf) = x
2323
2424 getProof : (x : Exists {a} P) -> P (getWitness x)
25− getProof (evidence x pf) = pf
25+ getProof (Evidence x pf) = pf
2626
2727 namespace Subset
2828 getWitness : Subset a P -> a
29− getWitness (element x pf) = x
29+ getWitness (Element x pf) = x
3030
3131 getProof : (x : Subset a P) -> P (getWitness x)
32− getProof (element x pf) = pf
32+ getProof (Element x pf) = pf
3333
3434 namespace Sigma
3535 getWitness : Sigma a P -> a
libs/prelude/Prelude/Strings.idr+2−2
@@ -74,11 +74,11 @@ data StrM : String -> Type where
7474 StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)
7575
7676||| 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
7878strHead' x p = assert_total $ prim__strHead x
7979
8080||| 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
8282strTail' x p = assert_total $ prim__strTail x
8383
8484-- 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
3737
3838||| Show that the length function on vectors in fact calculates the length
3939private lengthCorrect : (n : Nat) -> (xs : Vect n a) -> length xs = n
40−lengthCorrect Z [] = refl
41−lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in refl
40+lengthCorrect Z [] = Refl
41+lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl
4242
4343--------------------------------------------------------------------------------
4444-- Indexing into vectors
@@ -64,35 +64,36 @@ init (x::y::ys) = x :: init (y::ys)
6464
6565||| Extract a particular element from a vector
6666index : Fin n -> Vect n a -> a
67−index fZ (x::xs) = x
68−index (fS k) (x::xs) = index k xs
69−index fZ [] impossible
67+index FZ (x::xs) = x
68+index (FS k) (x::xs) = index k xs
69+index FZ [] impossible
70+
7071
7172||| Insert an element at a particular index
7273insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a
73−insertAt fZ y xs = y :: xs
74−insertAt (fS k) y (x::xs) = x :: insertAt k y xs
75−insertAt (fS k) y [] = absurd k
74+insertAt FZ y xs = y :: xs
75+insertAt (FS k) y (x::xs) = x :: insertAt k y xs
76+insertAt (FS k) y [] = absurd k
7677
7778||| Construct a new vector consisting of all but the indicated element
7879deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a
79−deleteAt fZ (x::xs) = xs
80−deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs
81−deleteAt {n = Z} (fS k) (x::xs) = absurd k
80+deleteAt FZ (x::xs) = xs
81+deleteAt {n = S m} (FS k) (x::xs) = x :: deleteAt k xs
82+deleteAt {n = Z} (FS k) (x::xs) = absurd k
8283deleteAt _ [] impossible
8384
8485||| Replace an element at a particlar index with another
8586replaceAt : Fin n -> t -> Vect n t -> Vect n t
86−replaceAt fZ y (x::xs) = y :: xs
87−replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs
87+replaceAt FZ y (x::xs) = y :: xs
88+replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
8889
8990||| Replace the element at a particular index with the result of applying a function to it
9091||| @ i the index to replace at
9192||| @ f the update function
9293||| @ xs the vector to replace in
9394updateAt : (i : Fin n) -> (f : t -> t) -> (xs : Vect n t) -> Vect n t
94−updateAt fZ f (x::xs) = f x :: xs
95−updateAt (fS k) f (x::xs) = x :: updateAt k f xs
95+updateAt FZ f (x::xs) = f x :: xs
96+updateAt (FS k) f (x::xs) = x :: updateAt k f xs
9697
9798--------------------------------------------------------------------------------
9899-- Subvectors
@@ -460,7 +461,7 @@ diag ((x::xs)::xss) = x :: diag (map tail xss)
460461
461462range : Vect n (Fin n)
462463range {n=Z} = []
463−range {n=S _} = fZ :: map fS range
464+range {n=S _} = FZ :: map FS range
464465
465466||| Transpose a Vect of Vects, turning rows into columns and vice versa.
466467|||
@@ -474,15 +475,15 @@ transpose (x :: xs) = zipWith (::) x (transpose xs)
474475--------------------------------------------------------------------------------
475476
476477vectConsCong : (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
478479
479480vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
480−vectNilRightNeutral [] = refl
481+vectNilRightNeutral [] = Refl
481482vectNilRightNeutral (x :: xs) =
482483 vectConsCong _ _ _ (vectNilRightNeutral xs)
483484
484485vectAppendAssociative : (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
486487vectAppendAssociative (x :: xs) ys zs =
487488 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
488489
samples/binary.idr+1−1
@@ -19,7 +19,7 @@ instance Show (Binary w k) where
1919 show (bin # bit) = show bin ++ show bit
2020
2121pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))
22−term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, refl)))
22+term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, Refl)))
2323
2424addBit : Bit x -> Bit y -> Bit c ->
2525 (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)
1414 (::) : interpTy a -> Env G -> Env (a :: G)
1515
1616-- data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
17−-- stop : HasType fZ (t :: G) t
18−-- pop : HasType k G t -> HasType (fS k) (u :: G) t
17+-- stop : HasType FZ (t :: G) t
18+-- pop : HasType k G t -> HasType (FS k) (u :: G) t
1919
2020 lookup : (i:Fin n) -> Env G -> interpTy (index i G)
21− lookup fZ (x :: xs) = x
22− lookup (fS i) (x :: xs) = lookup i xs
21+ lookup FZ (x :: xs) = x
22+ lookup (FS i) (x :: xs) = lookup i xs
2323
2424 data Expr : Vect n Ty -> Ty -> Type where
2525 Var : (i : Fin n) -> Expr G (index i G)
@@ -41,32 +41,32 @@ using (G : Vect n Ty)
4141 interp env (Bind v f) = interp env (f (interp env v))
4242
4343 eId : Expr G (TyFun TyInt TyInt)
44− eId = Lam (Var fZ)
44+ eId = Lam (Var FZ)
4545
4646 eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))
47− eTEST = Lam (Lam (Var (fS fZ)))
47+ eTEST = Lam (Lam (Var (FS FZ)))
4848
4949 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))))
5151
5252-- 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))
5454
5555 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))
5757
5858 app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
5959 app = \f, a => App f a
6060
6161 eFac : Expr G (TyFun TyInt TyInt)
62− eFac = Lam (If (Op (==) (Var fZ) (Val 0))
63− (Val 1) (Op (*) (app eFac (Op (-) (Var fZ) (Val 1))) (Var fZ)))
62+ eFac = Lam (If (Op (==) (Var FZ) (Val 0))
63+ (Val 1) (Op (*) (app eFac (Op (-) (Var FZ) (Val 1))) (Var FZ)))
6464
6565 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
6666
6767 eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt))
68− eProg = Lam (Lam (Bind (App eDouble (Var (fS fZ)))
69− (\x => Bind (App eDouble (Var fZ))
68+ eProg = Lam (Lam (Bind (App eDouble (Var (FS FZ)))
69+ (\x => Bind (App eDouble (Var FZ))
7070 (\y => Bind (App eDouble (Val x))
7171 (\z => App (App eAdd (Val y)) (Val z))))))
7272
samples/interp.idr+2−2
@@ -14,8 +14,8 @@ using (G : Vect n Ty)
1414 (::) : interpTy a -> Env G -> Env (a :: G)
1515
1616 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
17− stop : HasType fZ (t :: G) t
18− pop : HasType k G t -> HasType (fS k) (u :: G) t
17+ stop : HasType FZ (t :: G) t
18+ pop : HasType k G t -> HasType (FS k) (u :: G) t
1919
2020 lookup : HasType i G t -> Env G -> interpTy t
2121 lookup stop (x :: xs) = x
samples/reflection.idr+2−2
@@ -32,13 +32,13 @@ envList = ?envListPrf
3232
3333||| Reflected raw rep. for the type (TTName, TT)
3434tupleType : Raw
35−tupleType = RApp (RApp (Var (MN 0 "__Pair"))
35+tupleType = RApp (RApp (Var (UN "Pair"))
3636 (Var (NS (UN "TTName") ["Reflection", "Language"])))
3737 (Var (NS (UN "TT") ["Reflection", "Language"]))
3838
3939||| Reflected raw rep for the type List (TTName, TT)
4040mkTuple : Raw
41−mkTuple = RApp (RApp (Var (MN 0 "__MkPair"))
41+mkTuple = RApp (RApp (Var (UN "MkPair"))
4242 (Var (NS (UN "TTName") ["Reflection", "Language"])))
4343 (Var (NS (UN "TT") ["Reflection", "Language"]))
4444
src/Idris/AbsSyntaxTree.hs+9−39
@@ -1063,18 +1063,12 @@ getInferType (App (App _ ty) _) = ty
10631063
10641064
10651065
1066−-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
1066+-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
10671067
1068−primNames = [unitTy, unitCon,
1069− falseTy, pairTy, pairCon,
1070− eqTy, eqCon, inferTy, inferCon]
1068+primNames = [falseTy, eqTy, eqCon, inferTy, inferCon]
10711069
1072−unitDoc = parseDocstring . T.pack $ "The canonical single-element type, also known as the trivially true proposition."
1073−unitTy = sMN 0 "__Unit"
1074−unitCon = sMN 0 "__II"
1075−unitDecl = PDatadecl unitTy PType
1076− [(parseDocstring . T.pack $ "The trivial constructor for `()`. ", [], unitCon, PRef bi unitTy, bi, [])]
1077−unitOpts = [DefaultEliminator]
1070+unitTy = sUN "Unit"
1071+unitCon = sUN "MkUnit"
10781072
10791073falseDoc = parseDocstring . T.pack $
10801074 "The empty type, also known as the trivially false proposition." ++
@@ -1085,28 +1079,11 @@ falseTy = sMN 0 "__False"
10851079falseDecl = PDatadecl falseTy PType []
10861080falseOpts = []
10871081
1088−pairDoc = parseDocstring . T.pack $ "The non-dependent pair type, also known as conjunction."
1089−pairTy = sMN 0 "__Pair"
1090−pairCon = sMN 0 "__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
1082+pairTy = sUN "Pair"
1083+pairCon = sUN "MkPair"
11071084
11081085eqTy = sUN "="
1109−eqCon = sUN "refl"
1086+eqCon = sUN "Refl"
11101087eqDoc = parseDocstring . T.pack $
11111088 "The propositional equality type. A proof that `x` = `y`." ++
11121089 "\n\n" ++
@@ -1143,16 +1120,9 @@ eqParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left side of th
11431120
11441121eqOpts = []
11451122
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−
11531123-- Defined in builtins.idr
11541124sigmaTy = sUN "Sigma"
1155−existsCon = sUN "Sg_intro"
1125+existsCon = sUN "MkSigma"
11561126
11571127piBind :: [(Name, PTerm)] -> PTerm -> PTerm
11581128piBind = piBindp expl
@@ -1338,7 +1308,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
13381308
13391309 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
13401310 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"
13421312 prettySe p bnd (PResolveTC _) = text "resolvetc"
13431313 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
13441314 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
src/Idris/Apropos.hs+1−1
@@ -41,7 +41,7 @@ instance Apropos Name where
4141 | n == falseTy && str == T.pack "_|_" = True
4242 | (n == pairTy || n == pairCon) && str == T.pack "," = True
4343 | 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
4545 | (n == sigmaTy || n == existsCon) && str == T.pack "**" = True
4646 isApropos _ _ = False -- we don't care about case blocks, MNs, etc
4747
src/Idris/ElabDecls.hs+4−5
@@ -76,12 +76,11 @@ elabPrims :: Idris ()
7676elabPrims = do mapM_ (elabDecl' EAll recinfo)
7777 (map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)
7878 (zip4
79− [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
80− [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]
81− [emptyDocstring, unitDoc, falseDoc, pairDoc, eqDoc]
82− [[], [], [], pairParamDoc, eqParamDoc]))
79+ [inferOpts, falseOpts, eqOpts]
80+ [inferDecl, falseDecl, eqDecl]
81+ [emptyDocstring, falseDoc, eqDoc]
82+ [[], [], eqParamDoc]))
8383 addNameHint eqTy (sUN "prf")
84− elabDecl' EAll recinfo elimDecl
8584 mapM_ elabPrim primitives
8685 -- Special case prim__believe_me because it doesn't work on just constants
8786 elabBelieveMe
src/Idris/ElabTerm.hs+10−6
@@ -245,8 +245,12 @@ elab ist info emode opts fn tm
245245-- = lift $ tfail (Msg "Typecase is not allowed")
246246 elab' ina (PConstant c) = do apply (RConstant c) []; solve
247247 elab' ina (PQuote r) = do fill r; solve
248− elab' ina (PTrue fc _) = try (elab' ina (PRef fc unitCon))
249− (elab' ina (PRef fc unitTy))
248+ elab' ina (PTrue fc _) =
249+ do hnf_compute
250+ g <- goal
251+ case g of
252+ TType _ -> elab' ina (PRef fc unitTy)
253+ _ -> elab' ina (PRef fc unitCon)
250254 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
251255 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
252256 = do g <- goal; resolveTC False 5 g fn ist
@@ -283,11 +287,11 @@ elab ist info emode opts fn tm
283287 = do hnf_compute
284288 g <- goal
285289 case g of
286− TType _ -> elabE (True, a,inty, qq) (PApp fc (PRef fc pairTy)
290+ TType _ -> elab' ina (PApp fc (PRef fc pairTy)
287291 [pexp l,pexp r])
288− _ -> elabE (True, a, inty, qq) (PApp fc (PRef fc pairCon)
289− [pimp (sMN 0 "A") Placeholder True,
290− pimp (sMN 0 "B") Placeholder True,
292+ _ -> elab' ina (PApp fc (PRef fc pairCon)
293+ [pimp (sUN "A") Placeholder False,
294+ pimp (sUN "B") Placeholder False,
291295 pexp l, pexp r])
292296 elab' ina (PDPair fc p l@(PRef _ n) t r)
293297 = case t of
src/Idris/Erasure.hs+3−3
@@ -201,7 +201,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
201201
202202 -- these have been discovered as builtins but are not listed
203203 -- among Idris.Primitives.primitives
204− , mn "__MkPair" [2,3]
204+ --, mn "__MkPair" [2,3]
205205 , it "prim_fork" [0]
206206 , it "unsafePerformPrimIO" [1]
207207
@@ -348,8 +348,8 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
348348 -- assumed to be a global reference
349349 | otherwise = M.singleton cd (M.singleton (n, Result) S.empty)
350350 where
351− specialMNs = map (sMN 0 . ("__" ++)) $ words "Unit True False II"
352−
351+ specialMNs = [falseTy]
352+
353353 -- dependencies of de bruijn variables are described in `bs'
354354 getDepsTerm vs bs cd (V i) = snd (bs !! i) cd
355355
src/Idris/ParseExpr.hs+2−2
@@ -278,7 +278,7 @@ SimpleExpr ::=
278278 {- External (User-defined) Simple Expression -}
279279 | '?' Name
280280 | % 'instance'
281− | 'refl' ('{' Expr '}')?
281+ | 'Refl' ('{' Expr '}')?
282282 | ProofExpr
283283 | TacticsExpr
284284 | FnName
@@ -300,7 +300,7 @@ simpleExpr syn =
300300 try (simpleExternalExpr syn)
301301 <|> do x <- try (lchar '?' *> name); return (PMetavar x)
302302 <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)
303− <|> do reserved "refl"; fc <- getFC;
303+ <|> do reserved "Refl"; fc <- getFC;
304304 tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';
305305 return t)
306306 return (PRefl fc tm)
test/basic001/basic001a.idr+1−1
@@ -13,7 +13,7 @@ rle [] = REnd
1313rle (x :: xs) with (rle xs)
1414 rle (x :: []) | REnd = RChar 0 x REnd
1515 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)
1717 = RChar (S n) x rs
1818 rle (x :: (c :: (replicate n c ++ ys))) | (RChar n c rs) | (No f)
1919 = RChar 0 x (RChar n c rs)
test/basic001/reg005.idr+2−2
@@ -16,7 +16,7 @@ data RLE : Vect n Char -> Type where
1616 -> RLE (rep (S n) x ++ xs)
1717
1818eq : (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
2020
2121------------
2222
@@ -25,7 +25,7 @@ rle [] = REnd
2525rle (x :: xs) with (rle xs)
2626 rle (x :: Vect.Nil) | REnd = RChar Z x REnd
2727 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
2929 = RChar (S n) x rs
3030 rle (x :: rep (S n) y ++ ys) | RChar n y rs | Nothing
3131 = RChar Z x (RChar n y rs)
test/basic005/test019.lidr+6−6
@@ -1,16 +1,16 @@
11> module Main
22
3−> ifTrue : so True -> Nat
4−> ifTrue oh = S Z
3+> ifTrue : So True -> Nat
4+> ifTrue Oh = S Z
55
6−> ifFalse : so False -> Nat
7−> ifFalse oh impossible
6+> ifFalse : So False -> Nat
7+> ifFalse Oh impossible
88
9−> test : (f : Nat -> Bool) -> (n : Nat) -> so (f n) -> Nat
9+> test : (f : Nat -> Bool) -> (n : Nat) -> So (f n) -> Nat
1010> test f n x with (f n)
1111> | True = ifTrue x
1212> | False = ifFalse x
1313
1414> main : IO ()
15−> main = print (test ((S 4) ==) 5 oh)
15+> main = print (test ((S 4) ==) 5 Oh)
1616
test/basic009/Faulty.idr+1−1
@@ -4,4 +4,4 @@ import A
44import B.C
55
66fault : num = Z
7−fault = refl
7+fault = Refl
test/basic009/Main.idr+4−4
@@ -4,13 +4,13 @@ import A as X
44import B.C as Y
55
66checkX : X.num = Z
7−checkX = refl
7+checkX = Refl
88
99checkY : Y.num = S Z
10−checkY = refl
10+checkY = Refl
1111
1212checkAX : X.num = A.num
13−checkAX = refl
13+checkAX = Refl
1414
1515checkBY : 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
2020-- Here, the proof is very expensive to compute.
2121-- We add a recursive argument to prevent Idris from inlining the function.
2222f : (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
2424f (S r) n = f r n
2525
2626-- A (contrived) relation, just to have something to show.
@@ -30,7 +30,7 @@ data represents : Nat -> Nat -> Type where
3030-- Here, the witness is very expensive to compute.
3131-- We add a recursive argument to prevent Idris from inlining the function.
3232g : (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)
3434g (S r) n = g r n
3535
3636fmt : qib n `represents` n -> String
test/dsl001/test001.idr+3−3
@@ -14,8 +14,8 @@ using (G : Vect n Ty)
1414 (::) : interpTy a -> Env G -> Env (a :: G)
1515
1616 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
17− stop : HasType fZ (t :: G) t
18− pop : HasType k G t -> HasType (fS k) (u :: G) t
17+ stop : HasType FZ (t :: G) t
18+ pop : HasType k G t -> HasType (FS k) (u :: G) t
1919
2020 lookup : HasType i G t -> Env G -> interpTy t
2121 lookup stop (x :: xs) = x
@@ -58,7 +58,7 @@ using (G : Vect n Ty)
5858 eAdd = expr (\x, y => Op (+) x y)
5959
6060-- 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))
6262
6363 eDouble : Expr G (TyFun TyInt TyInt)
6464 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)
4646 interpTy (a :-> b) = a -> interpTy b
4747
4848 data HasType : Vect n Ty -> Fin n -> Ty -> Type where
49− stop : HasType (a :: gam) fZ a
50− pop : HasType gam i b -> HasType (a :: gam) (fS i) b
49+ stop : HasType (a :: gam) FZ a
50+ pop : HasType gam i b -> HasType (a :: gam) (FS i) b
5151
5252 data Env : Vect n Ty -> Type where
5353 Nil : Env Nil
test/dsl003/DSLPi.idr+5−5
@@ -6,7 +6,7 @@ dsl simple_type
66 pi = ARR
77
88test1 : simple_type (BOOL -> INT -> UNIT) = BOOL `ARR` (INT `ARR` UNIT)
9−test1 = refl
9+test1 = Refl
1010
1111using (vars : Vect n Ty)
1212 infix 2 ===
@@ -25,14 +25,14 @@ using (vars : Vect n Ty)
2525dsl specs
2626 pi = ForAll
2727 variable = Var
28− index_first = fZ
29− index_next = fS
28+ index_first = FZ
29+ index_next = FS
3030
3131test2 : Spec []
3232test2 = specs ((x, y : INT) -> x === y)
3333
3434test3 : 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
3636
3737test4 : 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 []
2−refl : ARR BOOL (ARR INT UNIT) = ARR BOOL (ARR INT UNIT)
1+ForAll INT (ForAll INT (ItHolds (Var (FS FZ) === Var FZ))) : Spec []
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
1616
1717testMemory : MemoryIO () () (Vect 4 Int)
1818testMemory = do Src :- allocate 5
19− Src :- poke 0 inpVect oh
19+ Src :- poke 0 inpVect Oh
2020 Dst :- allocate 5
21− Dst :- initialize (prim__truncInt_B8 1) 2 oh
22− move 2 2 3 oh oh
21+ Dst :- initialize (prim__truncInt_B8 1) 2 Oh
22+ move 2 2 3 Oh Oh
2323 Src :- free
24− end <- Dst :- peek 4 (S Z) oh
25− Dst :- poke 4 (sub1 end) oh
26− res <- Dst :- peek 1 (S(S(S(S Z)))) oh
24+ end <- Dst :- peek 4 (S Z) Oh
25+ Dst :- poke 4 (sub1 end) Oh
26+ res <- Dst :- peek 1 (S(S(S(S Z)))) Oh
2727 Dst :- free
2828 return (map (prim__zextB8_Int) res)
2929
test/error004/FunErrTest.idr+3−3
@@ -11,9 +11,9 @@ cadr : (xs : List a)
1111 -> {auto cons1 : isCons xs = True}
1212 -> {auto cons2 : isCons (tail xs) = True}
1313 -> a
14−cadr (x :: (y :: _)) {cons1=refl} {cons2=refl} = y
15−cadr (x :: []) {cons1=refl} {cons2=refl} impossible
16−cadr [] {cons1=refl} {cons2=refl} impossible
14+cadr (x :: (y :: _)) {cons1=Refl} {cons2=Refl} = y
15+cadr (x :: []) {cons1=Refl} {cons2=Refl} impossible
16+cadr [] {cons1=Refl} {cons2=Refl} impossible
1717
1818extractList : TT -> Maybe TT
1919extractList (App (App reflCon (App isCons lst)) _) = Just lst
test/ffi002/test023.idr+2−2
@@ -10,9 +10,9 @@ import Providers
1010goodProvider : IO (Provider Type)
1111goodProvider = return (Provide (the Type ()))
1212
13−%provide (Unit : Type) with goodProvider
13+%provide (Unit' : Type) with goodProvider
1414
15−foo : Unit
15+foo : Unit'
1616foo = ()
1717
1818-- Always fail
test/interactive001/expected+1−1
@@ -7,7 +7,7 @@ isElem x (y :: xs) = ?isElem_rhs_3
77f x :: map f xs
88isElem2 x (y :: ys) with (_)
99 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
1111
1212 [] => ?bar_1
1313 (x :: ys) => ?bar_2
test/io003/test018a.idr+5−5
@@ -4,17 +4,17 @@ import System.Concurrency.Process
44
55ping : ProcID String -> ProcID String -> Process String ()
66ping main proc
7− = do lift (usleep 1000)
7+ = do Lift (usleep 1000)
88 send proc "Hello!"
9− lift (putStrLn "Sent ping")
9+ Lift (putStrLn "Sent ping")
1010 msg <- recv
11− lift (putStrLn ("Reply: " ++ show msg))
11+ Lift (putStrLn ("Reply: " ++ show msg))
1212 send main "Done"
1313
1414pong : Process String ()
15−pong = do -- lift (putStrLn "Waiting for message")
15+pong = do -- Lift (putStrLn "Waiting for message")
1616 (sender, m) <- recvWithSender
17− lift $ putStrLn ("Received " ++ m)
17+ Lift $ putStrLn ("Received " ++ m)
1818 send sender ("Hello back!")
1919
2020mainProc : Process String ()
test/primitives003/test038.idr+5−5
@@ -2,7 +2,7 @@ module Main
22
33test : DecEq a => a -> a -> Bool
44test i1 i2 with (decEq i1 i2)
5− test i1 i1 | Yes refl = True
5+ test i1 i1 | Yes Refl = True
66 test i1 i2 | No p = False
77
88main : IO ()
@@ -52,10 +52,10 @@ main = do
5252 putStrLn . show $ test (Left "hello") (Right "world")
5353 putStrLn . show $ test (Left "hello") (Right False)
5454 -- Fin
55− putStrLn . show $ test (the (Fin (S (S (S (Z))))) (fS (fS (fZ))))
56− (the (Fin (S (S (S (Z))))) (fS (fS (fZ))))
57− putStrLn . show $ test (the (Fin (S (S (S (Z))))) (fS (fS (fZ))))
58− (the (Fin (S (S (S (Z))))) (fS (fZ)))
55+ putStrLn . show $ test (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
56+ (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
57+ putStrLn . show $ test (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
58+ (the (Fin (S (S (S (Z))))) (FS (FZ)))
5959 -- Nat
6060 putStrLn . show $ test (S (S (S Z))) (S (S (S Z)))
6161 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)
55-- Base case
66(Z + m = m + Z) <== plus_comm =
77 rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>
8− (Z + m = m) in refl
8+ (Z + m = m) in Refl
99
1010-- Step case
1111(S k + m = m + S k) <== plus_comm =
1212 rewrite ((k + m = m + k) <== plus_comm) in
1313 rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in
14− refl
14+ Refl
1515-- QED
1616
1717append : 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))
3636-- list appends
3737
3838 expr_r : Expr G xs -> (xs' ** (RExpr G xs', xs = xs'))
39− expr_r ENil = (_ ** (RNil, refl))
40− expr_r (Var i) = (_ ** (RApp RNil i, refl))
39+ expr_r ENil = (_ ** (RNil, Refl))
40+ expr_r (Var i) = (_ ** (RApp RNil i, Refl))
4141 expr_r (App ex ey) = let (xl ** (xr, xprf)) = expr_r ex in
4242 let (yl ** (yr, yprf)) = expr_r ey in
4343 appRExpr _ _ xr yr xprf yprf
@@ -47,7 +47,7 @@ using (xs : List a, ys : List a, G : List (List a))
4747 RExpr G xs -> RExpr G ys -> (xs' = xs) -> (ys' = ys) ->
4848 (ws' ** (RExpr G ws', xs' ++ ys' = ws'))
4949 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
5151 (_ ** (RApp rec i, ?appRExpr1))
5252 appRExpr x' y' rxs RNil xprf yprf = (_ ** (rxs, ?appRExpr2))
5353
@@ -68,12 +68,12 @@ using (xs : List a, ys : List a, G : List (List a))
6868 eqExpr : (e : Expr G xs) -> (e' : Expr G ys) ->
6969 Maybe (e = e')
7070 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
7272 eqExpr (App x y) (App x' y') | _ = Nothing
7373 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
7575 eqExpr (Var i) (Var j) | _ = Nothing
76− eqExpr ENil ENil = Just refl
76+ eqExpr ENil ENil = Just Refl
7777 eqExpr _ _ = Nothing
7878
7979-- 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))
8383 Expr G ln -> Expr G rn ->
8484 (xs = ln) -> (ys = rn) -> Maybe (xs = ys)
8585 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
8787 buildProof e e' lp rp | Nothing = Nothing
8888
8989 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))
108108 isElem : (x : a) -> (xs : List a) -> Maybe (Elem x xs)
109109 isElem x [] = Nothing
110110 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 |]
112112 isElem x (y :: ys) | Nothing = [| Pop (isElem x ys) |]
113113
114114 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))
126126-- %reflection means a function runs on syntax, rather than on constructors.
127127-- So, 'reflectList' builds a reflected List expression as defined above.
128128
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
130130-- reduction will work the right way.
131131
132132%reflection
test/proof003/test015.idr+1−1
@@ -45,7 +45,7 @@ testBin : Maybe (Binary 8 42)
4545testBin = natToBin _ _
4646
4747pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))
48−term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, refl)))
48+term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, Refl)))
4949
5050addBit : Bit x -> Bit y -> Bit c ->
5151 (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))))))
22--------------
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)))))
44--------------
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
44import Language.Reflection.Utils
55
66zzz2 : TT
7−zzz2 = `(fZ : Fin 3)
7+zzz2 = `(FZ : Fin 3)
88
99zzz : TT
10−zzz = `(fZ)
10+zzz = `(FZ)
test/quasiquote004/Quasiquote004.idr+1−1
@@ -24,7 +24,7 @@ data Fizzy : Nat -> Type where
2424-- Fizzy is a correct specification of divisibility by 3 - that is, if n is
2525-- fizzy then there exists some k such that n = 3*k.
2626fizzyCorrect : (n : Nat) -> Fizzy n -> (k : Nat ** n = 3 * k)
27−fizzyCorrect Z ZeroFizzy = (Z ** refl)
27+fizzyCorrect Z ZeroFizzy = (Z ** Refl)
2828fizzyCorrect (S (S (S k))) (Fizz x) =
2929 let (k' ** ih) = fizzyCorrect k x
3030 in (S k' ** ?fizzyIsAOK)
test/reg002/reg002.idr+2−2
@@ -17,10 +17,10 @@ S_Co_not_Inf : Main.S (Co n) = Infinity -> _|_
1717S_Co_not_Inf = believe_me
1818
1919S_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
2121S_inj (Co n) Infinity p = FalseElim (S_Co_not_Inf p)
2222S_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
2424
2525swap : {n : Nat} -> Vect n a -> Vect n a
2626swap Nil = Nil
test/reg006/reg006.idr+3−3
@@ -8,9 +8,9 @@ data RBTree : Type -> Type -> Nat -> Colour -> Type where
88 BlackBranch : k -> v -> RBTree k v n x -> RBTree k v n y -> RBTree k v (S n) Black
99
1010toBlack : 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))
12−toBlack Leaf = (_ ** (Leaf, Left refl))
13−toBlack (BlackBranch k v l r) = (_ ** (BlackBranch k v l r, Left refl))
11+toBlack (RedBranch k v l r) = (_ ** (BlackBranch k v l r, Right Refl))
12+toBlack Leaf = (_ ** (Leaf, Left Refl))
13+toBlack (BlackBranch k v l r) = (_ ** (BlackBranch k v l r, Left Refl))
1414
1515total
1616lookup : Ord k => k -> RBTree k v n Black -> Maybe v
test/reg007/reg007.lidr+1−1
@@ -3,7 +3,7 @@
33> import A
44
55> isSame : A.n = A.lala
6−> isSame = refl
6+> isSame = Refl
77
88> A.n = Z -- This is where it's at!
99> A.lala = S Z
test/reg009/reg009.lidr+6−6
@@ -4,15 +4,15 @@
44
55> filterTagP : (p : alpha -> Bool) ->
66> (as : Vect n alpha) ->
7−> so (isAnyBy p (n ** as)) ->
8−> (m : Nat ** (Vect m (a : alpha ** so (p a)), so (m > Z)))
7+> So (isAnyBy p (n ** as)) ->
8+> (m : Nat ** (Vect m (a : alpha ** So (p a)), So (m > Z)))
99> filterTagP {n = S m} p (a :: as) q with (p a)
1010> | True = (_
1111> **
12−> ((a ** believe_me oh)
12+> ((a ** believe_me Oh)
1313> ::
14−> (fst (getProof (filterTagP p as (believe_me oh)))),
15−> oh
14+> (fst (getProof (filterTagP p as (believe_me Oh)))),
15+> Oh
1616> )
1717> )
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) ->
2−> C True oh ->
3−> (b : Bool) -> (s : so b) -> (C b s)
4−> soElim C coh .True .oh = coh
1+> total soElim : (C : (b : Bool) -> So b -> Type) ->
2+> C True Oh ->
3+> (b : Bool) -> (s : So b) -> (C b s)
4+> soElim C coh .True .Oh = coh
55
6−> soFalseElim : so False -> a
6+> soFalseElim : So False -> a
77> soFalseElim x = FalseElim (soElim C () False x)
88> where
9−> C : (b : Bool) -> so b -> Type
9+> C : (b : Bool) -> So b -> Type
1010> C True s = ()
1111> C False s = _|_
1212
13−> soTrue : so b -> b = True
13+> soTrue : So b -> b = True
1414> soTrue {b = False} x = soFalseElim x
15−> soTrue {b = True} x = refl
15+> soTrue {b = True} x = Refl
1616
1717> class Eq alpha => ReflEqEq alpha where
18−> reflexive_eqeq : (a : alpha) -> so (a == a)
18+> reflexive_eqeq : (a : alpha) -> So (a == a)
1919
2020> modifyFun : (Eq alpha) =>
2121> (alpha -> beta) ->
@@ -28,7 +28,7 @@
2828> (ab : (alpha, beta)) ->
2929> modifyFun f ab (fst ab) = snd ab
3030> modifyFunLemma f (a,b) =
31−> rewrite soTrue (reflexive_eqeq a) in refl
31+> rewrite soTrue (reflexive_eqeq a) in Refl
3232
3333 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
22
33foo : { t : Type } ->
44 (a : t) ->
5− { default tactics { refine refl; solve; } prfA : a = a } ->
5+ { default tactics { refine Refl; solve; } prfA : a = a } ->
66 (b : Nat) ->
77 (c : Nat) ->
8− { default tactics { refine refl; solve; } prfBC : b = c } ->
8+ { default tactics { refine Refl; solve; } prfBC : b = c } ->
99 Nat
1010foo {t} a {prfA = p} b c {prfBC} = b
1111
test/reg018/reg018d.idr+3−3
@@ -3,10 +3,10 @@ module Main
33total
44pull : Fin (S n) -> Vect (S n) a -> (a, Vect n a)
55pull {n=Z} _ (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) =
6+-- pull {n=S q} FZ (Vect.(::) {n=S _} x xs) = (x, xs)
7+pull {n=S _} (FS n) (x :: xs) =
88 let (v, vs) = pull n xs in
99 (v, x::vs)
1010
1111main : 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))
2121FullBoard : Board n -> Type
2222FullBoard (MkBoard b) = All (All Filled) b
2323
24−indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (fS i) (x::xs)
25−indexStep = refl
24+indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (FS i) (x::xs)
25+indexStep = Refl
2626
2727find : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a)
2828 -> Either (All (\x => Not (P x)) xs) (y : a ** (P y, (i : Fin n ** y = index i xs)))
2929find _ Nil = Left Nil
3030find {P} d (x::xs) with (d x)
31− | Yes prf = Right (x ** (prf, (fZ ** refl)))
31+ | Yes prf = Right (x ** (prf, (FZ ** Refl)))
3232 | No prf =
3333 case find {P} d xs of
3434 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'')))
3636 Left prf' => Left (prf::prf')
3737
3838empty : (cell : Cell n) -> Dec (Empty cell)
39−empty Nothing = Yes refl
39+empty Nothing = Yes Refl
4040empty (Just _) = No nothingNotJust
4141
4242findEmptyInRow : (xs : Vect n (Cell n)) -> Either (All Filled xs) (i : Fin n ** Empty (index i xs))
@@ -60,11 +60,11 @@ emptyCell (MkBoard rs) =
6060 helper Nil = Left Nil
6161 helper (r::rs) =
6262 case findEmptyInRow r of
63− Right (ci ** pf3) => Right (fZ ** (ci ** pf3))
63+ Right (ci ** pf3) => Right (FZ ** (ci ** pf3))
6464 Left prf =>
6565 case helper rs of
6666 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))
6868
6969
7070main : IO ()
test/reg026/reg026.idr+1−1
@@ -1,7 +1,7 @@
11module Test
22
33X : Nat -> Type
4−X t = (c : Nat ** so (c < 5))
4+X t = (c : Nat ** So (c < 5))
55
66column : X t -> Nat
77column = getWitness
test/reg034/reg034.idr+2−2
@@ -3,8 +3,8 @@ import Prelude.List
33
44bar : (xs : List ()) -> (ys : List ()) ->
55 Prelude.List.length xs = Prelude.List.length ys -> xs = ys
6−bar xs xs refl = refl
6+bar xs xs Refl = Refl
77
88foo : (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
1010
test/reg035/reg035.idr+2−2
@@ -2,10 +2,10 @@ elimId : (a : Type) ->
22 (a1 : a) ->
33 (a2 : a) ->
44 (m : (x : a) -> (y : a) -> x = y -> Type) ->
5− (f : (x : a) -> m x x refl) ->
5+ (f : (x : a) -> m x x Refl) ->
66 (id : a1 = a2) ->
77 m a1 a2 id
8−elimId _ x _ _ f refl = f x
8+elimId _ x _ _ f Refl = f x
99
1010tran : (a : Type) -> (b : a) -> (c : a) -> (d : a) ->
1111 (e : b = c) -> (f : c = d) -> b = d
test/reg035/reg035a.lidr+7−7
@@ -6,9 +6,9 @@
66> (q : beta -> Bool) ->
77> (a : alpha) ->
88> (b : beta) ->
9−> so (p a) ->
10−> so (q b) ->
11−> so (p a && q b)
9+> So (p a) ->
10+> So (q b) ->
11+> So (p a && q b)
1212
1313> hasNoDuplicates : (Eq alpha) => List alpha -> Bool
1414> hasNoDuplicates as = as == nub as
@@ -33,7 +33,7 @@
3333
3434> postulate reflexive_Set_eqeq : (Eq a) =>
3535> (as : Set a) ->
36−> so (as == as)
36+> So (as == as)
3737
3838> unwrap : Set a -> List a
3939> unwrap (setify as) = as
@@ -53,14 +53,14 @@
5353
5454> partitionLemma0 : (Eq alpha) =>
5555> (ass : Set (Set alpha)) ->
56−> so (arePairwiseDisjoint ass) ->
57−> so (ass `isPartition` union ass)
56+> So (arePairwiseDisjoint ass) ->
57+> So (ass `isPartition` union ass)
5858> partitionLemma0 ass asspd = (soAndIntro (\ xss => arePairwiseDisjoint xss)
5959> (\ xs => union ass == xs)
6060> ass
6161> (union ass)
6262> asspd
6363> uasseqas) where
64−> uasseqas : so (union ass == union ass)
64+> uasseqas : So (union ass == union ass)
6565> uasseqas = reflexive_Set_eqeq (union ass)
6666
test/reg044/reg044.idr+1−1
@@ -3,4 +3,4 @@ exjection = ?pf
33
44pf = proof
55 intros
6− refine refl
6+ refine Refl
test/reg047/reg047.idr+3−3
@@ -8,11 +8,11 @@ data Nat = zero | succ Nat
88Id : (A : Type) -> A -> A -> Type
99Id A = (=) {a0 = A} {b0 = A}
1010
11−Refl : (A : Type) -> (a : A) -> Id A a a
12−Refl A a = refl {a}
11+IdRefl : (A : Type) -> (a : A) -> Id A a a
12+IdRefl A a = Refl {a}
1313
1414zzz : Id Nat zero zero
15−zzz = Refl Nat zero
15+zzz = IdRefl Nat zero
1616
1717eep : TTSigma Nat (\ a => Id Nat a zero)
1818eep = sigma Nat (\ a => Id Nat a zero) zero zzz
test/reg047/reg047a.idr+4−4
@@ -8,17 +8,17 @@ data MNat = zero | succ MNat
88Id : (A : Type) -> A -> A -> Type
99Id = \A,x,y => x = y -- {a = A} {b = A}
1010
11−Refl : (A : Type) -> (a : A) -> Id A a a
12−Refl A a = refl {a}
11+IdRefl : (A : Type) -> (a : A) -> Id A a a
12+IdRefl A a = Refl {a}
1313
1414zzzz : Id MNat zero zero
15−zzzz = Refl MNat zero
15+zzzz = IdRefl MNat zero
1616
1717eep : TTSigma MNat (\ c => Id MNat c zero)
1818eep = (sigma MNat (\b => Id MNat b zero) zero zzzz)
1919
2020eep2 : 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))
2222
2323
2424
test/totality002/test017.idr+3−3
@@ -82,9 +82,9 @@ mfib (S (S n)) = mfib (S n) + mfib n
8282
8383maxCommutative : (left : Nat) -> (right : Nat) ->
8484 maximum left right = maximum right left
85−maxCommutative Z Z = refl
86−maxCommutative (S left) Z = refl
87−maxCommutative Z (S right) = refl
85+maxCommutative Z Z = Refl
86+maxCommutative (S left) Z = Refl
87+maxCommutative Z (S right) = Refl
8888maxCommutative (S left) (S right) =
8989 let inductiveHypothesis = maxCommutative left right in
9090 ?maxCommutativeStepCase
test/totality006/expected+1−1
@@ -1,2 +1,2 @@
11totality006.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
2−antitrue oh impossible
1+antitrue : So False -> a
2+antitrue Oh impossible
33
44total
5−prf : (a:Nat) -> (b:Nat) -> so (a > b) -> GT a b
6−prf Z Z oh impossible
5+prf : (a:Nat) -> (b:Nat) -> So (a > b) -> GT a b
6+prf Z Z Oh impossible
77prf Z (S k) um = antitrue um
8−prf (S k) Z um = lteSucc lteZero
9−-- prf (S _) (S _) oh impossible
8+prf (S k) Z um = LTESucc LTEZero
9+-- prf (S _) (S _) Oh impossible
1010
1111
test/totality006/totality006a.idr+6−6
@@ -1,10 +1,10 @@
1−antitrue : so False -> a
2−antitrue oh impossible
1+antitrue : So False -> a
2+antitrue Oh impossible
33
44total
5−prf' : (a:Nat) -> (b:Nat) -> so (a > b) -> GT a b
6−prf' Z Z oh impossible
5+prf' : (a:Nat) -> (b:Nat) -> So (a > b) -> GT a b
6+prf' Z Z Oh impossible
77prf' Z (S k) um = antitrue um
8−prf' (S k) Z um = lteSucc lteZero
9−prf' (S _) (S _) oh impossible
8+prf' (S k) Z um = LTESucc LTEZero
9+prf' (S _) (S _) Oh impossible
1010
test/tutorial004/tutorial004.idr+5−5
@@ -1,9 +1,9 @@
11
22fiveIsFive : 5 = 5
3−fiveIsFive = refl
3+fiveIsFive = Refl
44
55twoPlusTwo : 2 + 2 = 4
6−twoPlusTwo = refl
6+twoPlusTwo = Refl
77
88total disjoint : (n : Nat) -> Z = S n -> _|_
99disjoint n p = replace {P = disjointTy} p ()
@@ -25,14 +25,14 @@ empty2 : _|_
2525empty2 = empty2
2626
2727plusReduces : (n:Nat) -> plus Z n = n
28−plusReduces n = refl
28+plusReduces n = Refl
2929
3030plusReducesZ : (n:Nat) -> n = plus n Z
31−plusReducesZ Z = refl
31+plusReducesZ Z = Refl
3232plusReducesZ (S k) = cong (plusReducesZ k)
3333
3434plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
35−plusReducesS Z m = refl
35+plusReducesS Z m = Refl
3636plusReducesS (S k) m = cong (plusReducesS k m)
3737
3838plusReducesZ' : (n:Nat) -> n = plus n Z