git.iko.soy/Idris-dev
on master help sign in
rename O into Z
commit2311d5501376182d52dae4d1579e7fc189d378b4 authorraichoo <raichoo@googlemail.com> dateFri 26 Jul 2013, 21:05 (13 years ago) parentc330406
50 files changed+422−422
compare with master
unifiedsplit
effects/Effect/Memory.idr+1−1 effects/Effects.idr+2−2 lib/Data/Bits.idr+102−102 lib/Data/BoundedList.idr+3−3 lib/Data/HVect.idr+1−1 lib/Data/SortedMap.idr+6−6 lib/Data/Vect.idr+1−1 lib/Data/ZZ.idr+6−6 lib/Decidable/Equality.idr+4−4 lib/Decidable/Order.idr+3−3 lib/Prelude.idr+1−1 lib/Prelude/Fin.idr+3−3 lib/Prelude/Heap.idr+2−2 lib/Prelude/List.idr+5−5 lib/Prelude/Nat.idr+105−105 lib/Prelude/Vect.idr+3−3 lib/Uninhabited.idr+2−2 samples/binary.idr+2−2 src/IRTS/Compiler.hs+3−3 src/Idris/AbsSyntaxTree.hs+2−2 src/Idris/Transforms.hs+1−1 test/reg001/reg001.idr+1−1 test/reg004/reg004.idr+2−2 test/reg005/reg005.idr+3−3 test/reg006/reg006.idr+1−1 test/reg008/reg008.idr+3−3 test/reg009/reg009.lidr+1−1 test/reg010/reg010.idr+1−1 test/reg011/reg011.idr+2−2 test/reg018/reg018b.idr+3−3 test/reg018/reg018c.idr+1−1 test/reg018/reg018d.idr+1−1 test/test005/test005.idr+1−1 test/test006/test006.idr+3−3 test/test015/Parity.idr+2−2 test/test015/test015.idr+6−6 test/test016/test016.idr+1−1 test/test017/test017.idr+16−16 test/test019/test019.lidr+1−1 test/test025/test025.idr+2−2 tutorial/classes.tex+8−8 tutorial/examples/binary.idr+6−6 tutorial/examples/theorems.idr+14−14 tutorial/examples/usefultypes.idr+1−1 tutorial/examples/views.idr+3−3 tutorial/examples/wheres.idr+3−3 tutorial/provisional.tex+6−6 tutorial/theorems.tex+46−46 tutorial/typesfuns.tex+24−24 tutorial/views.tex+2−2
effects/Effect/Memory.idr+1−1
@@ -63,7 +63,7 @@ do_memmove dest src dest_offset src_offset size
6363
6464private
6565do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect Bits8 size)
66−do_peek _ _ O = return (Prelude.Vect.Nil)
66+do_peek _ _ Z = return (Prelude.Vect.Nil)
6767do_peek ptr offset (S n)
6868 = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FByte) ptr (fromInteger $ cast offset)
6969 bs <- do_peek ptr (S offset) n
effects/Effects.idr+2−2
@@ -63,13 +63,13 @@ rebuildEnv (x :: xs) SubNil [] = x :: xs
6363
6464-- some proof automation
6565findEffElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic -- Nat is maximum search depth
66−findEffElem O ctxt goal = Refine "Here" `Seq` Solve
66+findEffElem Z ctxt goal = Refine "Here" `Seq` Solve
6767findEffElem (S n) ctxt goal = GoalType "EffElem"
6868 (Try (Refine "Here" `Seq` Solve)
6969 (Refine "There" `Seq` (Solve `Seq` findEffElem n ctxt goal)))
7070
7171findSubList : Nat -> List (TTName, Binder TT) -> TT -> Tactic
72−findSubList O ctxt goal = Refine "SubNil" `Seq` Solve
72+findSubList Z ctxt goal = Refine "SubNil" `Seq` Solve
7373findSubList (S n) ctxt goal
7474 = GoalType "SubList"
7575 (Try (Refine "subListId" `Seq` Solve)
lib/Data/Bits.idr+102−102
@@ -4,11 +4,11 @@ module Data.Bits
44
55divCeil : Nat -> Nat -> Nat
66divCeil x y = case x `mod` y of
7− O => x `div` y
7+ Z => x `div` y
88 S _ => S (x `div` y)
99
1010nextPow2 : Nat -> Nat
11−nextPow2 O = O
11+nextPow2 Z = Z
1212nextPow2 x = if x == (2 `power` l2x)
1313 then l2x
1414 else S l2x
@@ -19,9 +19,9 @@ nextBytes : Nat -> Nat
1919nextBytes bits = (nextPow2 (bits `divCeil` 8))
2020
2121machineTy : Nat -> Type
22−machineTy O = Bits8
23−machineTy (S O) = Bits16
24−machineTy (S (S O)) = Bits32
22+machineTy Z = Bits8
23+machineTy (S Z) = Bits16
24+machineTy (S (S Z)) = Bits32
2525machineTy (S (S (S _))) = Bits64
2626
2727bitsUsed : Nat -> Nat
@@ -29,19 +29,19 @@ bitsUsed n = 8 * (2 `power` n)
2929
3030%assert_total
3131natToBits' : machineTy n -> Nat -> machineTy n
32−natToBits' a O = a
32+natToBits' a Z = a
3333natToBits' {n=n} a x with n
3434 -- it seems I have to manually recover the value of n here, instead of being able to reference it
35− natToBits' a (S x') | O = natToBits' {n=0} (prim__addB8 a (prim__truncInt_B8 1)) x'
36− natToBits' a (S x') | S O = natToBits' {n=1} (prim__addB16 a (prim__truncInt_B16 1)) x'
37− natToBits' a (S x') | S (S O) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x'
35+ natToBits' a (S x') | Z = natToBits' {n=0} (prim__addB8 a (prim__truncInt_B8 1)) x'
36+ natToBits' a (S x') | S Z = natToBits' {n=1} (prim__addB16 a (prim__truncInt_B16 1)) x'
37+ natToBits' a (S x') | S (S Z) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x'
3838 natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'
3939
4040natToBits : Nat -> machineTy n
4141natToBits {n=n} x with n
42− | O = natToBits' {n=0} (prim__truncInt_B8 0) x
43− | S O = natToBits' {n=1} (prim__truncInt_B16 0) x
44− | S (S O) = natToBits' {n=2} (prim__truncInt_B32 0) x
42+ | Z = natToBits' {n=0} (prim__truncInt_B8 0) x
43+ | S Z = natToBits' {n=1} (prim__truncInt_B16 0) x
44+ | S (S Z) = natToBits' {n=2} (prim__truncInt_B32 0) x
4545 | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x
4646
4747getPad : Nat -> machineTy n
@@ -94,9 +94,9 @@ pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad
9494
9595shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
9696shiftLeft' {n=n} x c with (nextBytes n)
97− | O = pad8' n prim__shlB8 x c
98− | S O = pad16' n prim__shlB16 x c
99− | S (S O) = pad32' n prim__shlB32 x c
97+ | Z = pad8' n prim__shlB8 x c
98+ | S Z = pad16' n prim__shlB16 x c
99+ | S (S Z) = pad32' n prim__shlB32 x c
100100 | S (S (S _)) = pad64' n prim__shlB64 x c
101101
102102public
@@ -105,9 +105,9 @@ shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
105105
106106shiftRightLogical' : machineTy n -> machineTy n -> machineTy n
107107shiftRightLogical' {n=n} x c with n
108− | O = prim__lshrB8 x c
109− | S O = prim__lshrB16 x c
110− | S (S O) = prim__lshrB32 x c
108+ | Z = prim__lshrB8 x c
109+ | S Z = prim__lshrB16 x c
110+ | S (S Z) = prim__lshrB32 x c
111111 | S (S (S _)) = prim__lshrB64 x c
112112
113113public
@@ -117,9 +117,9 @@ shiftRightLogical {n} (MkBits x) (MkBits y)
117117
118118shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
119119shiftRightArithmetic' {n=n} x c with (nextBytes n)
120− | O = pad8' n prim__ashrB8 x c
121− | S O = pad16' n prim__ashrB16 x c
122− | S (S O) = pad32' n prim__ashrB32 x c
120+ | Z = pad8' n prim__ashrB8 x c
121+ | S Z = pad16' n prim__ashrB16 x c
122+ | S (S Z) = pad32' n prim__ashrB32 x c
123123 | S (S (S _)) = pad64' n prim__ashrB64 x c
124124
125125public
@@ -128,9 +128,9 @@ shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
128128
129129and' : machineTy n -> machineTy n -> machineTy n
130130and' {n=n} x y with n
131− | O = prim__andB8 x y
132− | S O = prim__andB16 x y
133− | S (S O) = prim__andB32 x y
131+ | Z = prim__andB8 x y
132+ | S Z = prim__andB16 x y
133+ | S (S Z) = prim__andB32 x y
134134 | S (S (S _)) = prim__andB64 x y
135135
136136public
@@ -139,9 +139,9 @@ and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)
139139
140140or' : machineTy n -> machineTy n -> machineTy n
141141or' {n=n} x y with n
142− | O = prim__orB8 x y
143− | S O = prim__orB16 x y
144− | S (S O) = prim__orB32 x y
142+ | Z = prim__orB8 x y
143+ | S Z = prim__orB16 x y
144+ | S (S Z) = prim__orB32 x y
145145 | S (S (S _)) = prim__orB64 x y
146146
147147public
@@ -150,9 +150,9 @@ or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)
150150
151151xor' : machineTy n -> machineTy n -> machineTy n
152152xor' {n=n} x y with n
153− | O = prim__xorB8 x y
154− | S O = prim__xorB16 x y
155− | S (S O) = prim__xorB32 x y
153+ | Z = prim__xorB8 x y
154+ | S Z = prim__xorB16 x y
155+ | S (S Z) = prim__xorB32 x y
156156 | S (S (S _)) = prim__xorB64 x y
157157
158158public
@@ -161,9 +161,9 @@ xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)
161161
162162plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
163163plus' {n=n} x y with (nextBytes n)
164− | O = pad8 n prim__addB8 x y
165− | S O = pad16 n prim__addB16 x y
166− | S (S O) = pad32 n prim__addB32 x y
164+ | Z = pad8 n prim__addB8 x y
165+ | S Z = pad16 n prim__addB16 x y
166+ | S (S Z) = pad32 n prim__addB32 x y
167167 | S (S (S _)) = pad64 n prim__addB64 x y
168168
169169public
@@ -172,9 +172,9 @@ plus (MkBits x) (MkBits y) = MkBits (plus' x y)
172172
173173minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
174174minus' {n=n} x y with (nextBytes n)
175− | O = pad8 n prim__subB8 x y
176− | S O = pad16 n prim__subB16 x y
177− | S (S O) = pad32 n prim__subB32 x y
175+ | Z = pad8 n prim__subB8 x y
176+ | S Z = pad16 n prim__subB16 x y
177+ | S (S Z) = pad32 n prim__subB32 x y
178178 | S (S (S _)) = pad64 n prim__subB64 x y
179179
180180public
@@ -183,9 +183,9 @@ minus (MkBits x) (MkBits y) = MkBits (minus' x y)
183183
184184times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
185185times' {n=n} x y with (nextBytes n)
186− | O = pad8 n prim__mulB8 x y
187− | S O = pad16 n prim__mulB16 x y
188− | S (S O) = pad32 n prim__mulB32 x y
186+ | Z = pad8 n prim__mulB8 x y
187+ | S Z = pad16 n prim__mulB16 x y
188+ | S (S Z) = pad32 n prim__mulB32 x y
189189 | S (S (S _)) = pad64 n prim__mulB64 x y
190190
191191public
@@ -195,9 +195,9 @@ times (MkBits x) (MkBits y) = MkBits (times' x y)
195195partial
196196sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
197197sdiv' {n=n} x y with (nextBytes n)
198− | O = prim__sdivB8 x y
199− | S O = prim__sdivB16 x y
200− | S (S O) = prim__sdivB32 x y
198+ | Z = prim__sdivB8 x y
199+ | S Z = prim__sdivB16 x y
200+ | S (S Z) = prim__sdivB32 x y
201201 | S (S (S _)) = prim__sdivB64 x y
202202
203203public partial
@@ -207,9 +207,9 @@ sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)
207207partial
208208udiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
209209udiv' {n=n} x y with (nextBytes n)
210− | O = prim__udivB8 x y
211− | S O = prim__udivB16 x y
212− | S (S O) = prim__udivB32 x y
210+ | Z = prim__udivB8 x y
211+ | S Z = prim__udivB16 x y
212+ | S (S Z) = prim__udivB32 x y
213213 | S (S (S _)) = prim__udivB64 x y
214214
215215public partial
@@ -219,9 +219,9 @@ udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)
219219partial
220220srem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
221221srem' {n=n} x y with (nextBytes n)
222− | O = prim__sremB8 x y
223− | S O = prim__sremB16 x y
224− | S (S O) = prim__sremB32 x y
222+ | Z = prim__sremB8 x y
223+ | S Z = prim__sremB16 x y
224+ | S (S Z) = prim__sremB32 x y
225225 | S (S (S _)) = prim__sremB64 x y
226226
227227public partial
@@ -231,9 +231,9 @@ srem (MkBits x) (MkBits y) = MkBits (srem' x y)
231231partial
232232urem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
233233urem' {n=n} x y with (nextBytes n)
234− | O = prim__uremB8 x y
235− | S O = prim__uremB16 x y
236− | S (S O) = prim__uremB32 x y
234+ | Z = prim__uremB8 x y
235+ | S Z = prim__uremB16 x y
236+ | S (S Z) = prim__uremB32 x y
237237 | S (S (S _)) = prim__uremB64 x y
238238
239239public partial
@@ -243,37 +243,37 @@ urem (MkBits x) (MkBits y) = MkBits (urem' x y)
243243-- TODO: Proofy comparisons via postulates
244244lt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
245245lt {n=n} x y with (nextBytes n)
246− | O = prim__ltB8 x y
247− | S O = prim__ltB16 x y
248− | S (S O) = prim__ltB32 x y
246+ | Z = prim__ltB8 x y
247+ | S Z = prim__ltB16 x y
248+ | S (S Z) = prim__ltB32 x y
249249 | S (S (S _)) = prim__ltB64 x y
250250
251251lte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
252252lte {n=n} x y with (nextBytes n)
253− | O = prim__lteB8 x y
254− | S O = prim__lteB16 x y
255− | S (S O) = prim__lteB32 x y
253+ | Z = prim__lteB8 x y
254+ | S Z = prim__lteB16 x y
255+ | S (S Z) = prim__lteB32 x y
256256 | S (S (S _)) = prim__lteB64 x y
257257
258258eq : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
259259eq {n=n} x y with (nextBytes n)
260− | O = prim__eqB8 x y
261− | S O = prim__eqB16 x y
262− | S (S O) = prim__eqB32 x y
260+ | Z = prim__eqB8 x y
261+ | S Z = prim__eqB16 x y
262+ | S (S Z) = prim__eqB32 x y
263263 | S (S (S _)) = prim__eqB64 x y
264264
265265gte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
266266gte {n=n} x y with (nextBytes n)
267− | O = prim__gteB8 x y
268− | S O = prim__gteB16 x y
269− | S (S O) = prim__gteB32 x y
267+ | Z = prim__gteB8 x y
268+ | S Z = prim__gteB16 x y
269+ | S (S Z) = prim__gteB32 x y
270270 | S (S (S _)) = prim__gteB64 x y
271271
272272gt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
273273gt {n=n} x y with (nextBytes n)
274− | O = prim__gtB8 x y
275− | S O = prim__gtB16 x y
276− | S (S O) = prim__gtB32 x y
274+ | Z = prim__gtB8 x y
275+ | S Z = prim__gtB16 x y
276+ | S (S Z) = prim__gtB32 x y
277277 | S (S (S _)) = prim__gtB64 x y
278278
279279instance Eq (Bits n) where
@@ -293,11 +293,11 @@ instance Ord (Bits n) where
293293
294294complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)
295295complement' {n=n} x with (nextBytes n)
296− | O = let pad = getPad {n=0} n in
296+ | Z = let pad = getPad {n=0} n in
297297 prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad
298− | S O = let pad = getPad {n=1} n in
298+ | S Z = let pad = getPad {n=1} n in
299299 prim__complB16 (x `prim__shlB16` pad) `prim__lshrB16` pad
300− | S (S O) = let pad = getPad {n=2} n in
300+ | S (S Z) = let pad = getPad {n=2} n in
301301 prim__complB32 (x `prim__shlB32` pad) `prim__lshrB32` pad
302302 | S (S (S _)) = let pad = getPad {n=3} n in
303303 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
@@ -309,15 +309,15 @@ complement (MkBits x) = MkBits (complement' x)
309309-- TODO: Prove
310310zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
311311zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
312− | (O, O) = believe_me x
313− | (O, S O) = believe_me (prim__zextB8_B16 (believe_me x))
314− | (O, S (S O)) = believe_me (prim__zextB8_B32 (believe_me x))
315− | (O, S (S (S _))) = believe_me (prim__zextB8_B64 (believe_me x))
316− | (S O, S O) = believe_me x
317− | (S O, S (S O)) = believe_me (prim__zextB16_B32 (believe_me x))
318− | (S O, S (S (S _))) = believe_me (prim__zextB16_B64 (believe_me x))
319− | (S (S O), S (S O)) = believe_me x
320− | (S (S O), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))
312+ | (Z, Z) = believe_me x
313+ | (Z, S Z) = believe_me (prim__zextB8_B16 (believe_me x))
314+ | (Z, S (S Z)) = believe_me (prim__zextB8_B32 (believe_me x))
315+ | (Z, S (S (S _))) = believe_me (prim__zextB8_B64 (believe_me x))
316+ | (S Z, S Z) = believe_me x
317+ | (S Z, S (S Z)) = believe_me (prim__zextB16_B32 (believe_me x))
318+ | (S Z, S (S (S _))) = believe_me (prim__zextB16_B64 (believe_me x))
319+ | (S (S Z), S (S Z)) = believe_me x
320+ | (S (S Z), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))
321321 | (S (S (S _)), S (S (S _))) = believe_me x
322322
323323public
@@ -327,11 +327,11 @@ zeroExtend (MkBits x) = MkBits (zext' x)
327327%assert_total
328328intToBits' : Integer -> machineTy (nextBytes n)
329329intToBits' {n=n} x with (nextBytes n)
330− | O = let pad = getPad {n=0} n in
330+ | Z = let pad = getPad {n=0} n in
331331 prim__lshrB8 (prim__shlB8 (prim__truncBigInt_B8 x) pad) pad
332− | S O = let pad = getPad {n=1} n in
332+ | S Z = let pad = getPad {n=1} n in
333333 prim__lshrB16 (prim__shlB16 (prim__truncBigInt_B16 x) pad) pad
334− | S (S O) = let pad = getPad {n=2} n in
334+ | S (S Z) = let pad = getPad {n=2} n in
335335 prim__lshrB32 (prim__shlB32 (prim__truncBigInt_B32 x) pad) pad
336336 | S (S (S _)) = let pad = getPad {n=3} n in
337337 prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad
@@ -345,9 +345,9 @@ instance Cast Integer (Bits n) where
345345
346346bitsToInt' : machineTy (nextBytes n) -> Integer
347347bitsToInt' {n=n} x with (nextBytes n)
348− | O = prim__zextB8_BigInt x
349− | S O = prim__zextB16_BigInt x
350− | S (S O) = prim__zextB32_BigInt x
348+ | Z = prim__zextB8_BigInt x
349+ | S Z = prim__zextB16_BigInt x
350+ | S (S Z) = prim__zextB32_BigInt x
351351 | S (S (S _)) = prim__zextB64_BigInt x
352352
353353public
@@ -364,28 +364,28 @@ bitsToInt (MkBits x) = bitsToInt' x
364364-- TODO: Prove
365365sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
366366sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
367− | (O, O) = let pad = getPad {n=0} n in
367+ | (Z, Z) = let pad = getPad {n=0} n in
368368 believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)
369− | (O, S O) = let pad = getPad {n=0} n in
369+ | (Z, S Z) = let pad = getPad {n=0} n in
370370 believe_me (prim__ashrB16 (prim__sextB8_B16 (prim__shlB8 (believe_me x) pad))
371371 (prim__zextB8_B16 pad))
372− | (O, S (S O)) = let pad = getPad {n=0} n in
372+ | (Z, S (S Z)) = let pad = getPad {n=0} n in
373373 believe_me (prim__ashrB32 (prim__sextB8_B32 (prim__shlB8 (believe_me x) pad))
374374 (prim__zextB8_B32 pad))
375− | (O, S (S (S _))) = let pad = getPad {n=0} n in
375+ | (Z, S (S (S _))) = let pad = getPad {n=0} n in
376376 believe_me (prim__ashrB64 (prim__sextB8_B64 (prim__shlB8 (believe_me x) pad))
377377 (prim__zextB8_B64 pad))
378− | (S O, S O) = let pad = getPad {n=1} n in
378+ | (S Z, S Z) = let pad = getPad {n=1} n in
379379 believe_me (prim__ashrB16 (prim__shlB16 (believe_me x) pad) pad)
380− | (S O, S (S O)) = let pad = getPad {n=1} n in
380+ | (S Z, S (S Z)) = let pad = getPad {n=1} n in
381381 believe_me (prim__ashrB32 (prim__sextB16_B32 (prim__shlB16 (believe_me x) pad))
382382 (prim__zextB16_B32 pad))
383− | (S O, S (S (S _))) = let pad = getPad {n=1} n in
383+ | (S Z, S (S (S _))) = let pad = getPad {n=1} n in
384384 believe_me (prim__ashrB64 (prim__sextB16_B64 (prim__shlB16 (believe_me x) pad))
385385 (prim__zextB16_B64 pad))
386− | (S (S O), S (S O)) = let pad = getPad {n=2} n in
386+ | (S (S Z), S (S Z)) = let pad = getPad {n=2} n in
387387 believe_me (prim__ashrB32 (prim__shlB32 (believe_me x) pad) pad)
388− | (S (S O), S (S (S _))) = let pad = getPad {n=2} n in
388+ | (S (S Z), S (S (S _))) = let pad = getPad {n=2} n in
389389 believe_me (prim__ashrB64 (prim__sextB32_B64 (prim__shlB32 (believe_me x) pad))
390390 (prim__zextB32_B64 pad))
391391 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in
@@ -398,15 +398,15 @@ sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
398398-- TODO: Prove
399399trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)
400400trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
401− | (O, O) = believe_me x
402− | (O, S O) = believe_me (prim__truncB16_B8 (believe_me x))
403− | (O, S (S O)) = believe_me (prim__truncB32_B8 (believe_me x))
404− | (O, S (S (S _))) = believe_me (prim__truncB64_B8 (believe_me x))
405− | (S O, S O) = believe_me x
406− | (S O, S (S O)) = believe_me (prim__truncB32_B16 (believe_me x))
407− | (S O, S (S (S _))) = believe_me (prim__truncB64_B16 (believe_me x))
408− | (S (S O), S (S O)) = believe_me x
409− | (S (S O), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))
401+ | (Z, Z) = believe_me x
402+ | (Z, S Z) = believe_me (prim__truncB16_B8 (believe_me x))
403+ | (Z, S (S Z)) = believe_me (prim__truncB32_B8 (believe_me x))
404+ | (Z, S (S (S _))) = believe_me (prim__truncB64_B8 (believe_me x))
405+ | (S Z, S Z) = believe_me x
406+ | (S Z, S (S Z)) = believe_me (prim__truncB32_B16 (believe_me x))
407+ | (S Z, S (S (S _))) = believe_me (prim__truncB64_B16 (believe_me x))
408+ | (S (S Z), S (S Z)) = believe_me x
409+ | (S (S Z), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))
410410 | (S (S (S _)), S (S (S _))) = believe_me x
411411
412412--public
lib/Data/BoundedList.idr+3−3
@@ -34,7 +34,7 @@ weaken (x :: xs) = x :: weaken xs
3434
3535take : (n : Nat) -> List a -> BoundedList a n
3636take _ [] = []
37−take O _ = []
37+take Z _ = []
3838take (S n') (x :: xs) = x :: take n' xs
3939
4040toList : BoundedList a n -> List a
@@ -50,7 +50,7 @@ fromList (x :: xs) = x :: fromList xs
5050--------------------------------------------------------------------------------
5151
5252replicate : (n : Nat) -> a -> BoundedList a n
53−replicate O _ = []
53+replicate Z _ = []
5454replicate (S n) x = x :: replicate n x
5555
5656--------------------------------------------------------------------------------
@@ -79,7 +79,7 @@ map f (x :: xs) = f x :: map f xs
7979
8080%assert_total -- not sure why this isn't accepted - clearly decreasing on n
8181pad : (xs : BoundedList a n) -> (padding : a) -> BoundedList a n
82−pad {n=O} [] _ = []
82+pad {n=Z} [] _ = []
8383pad {n=S n'} [] padding = padding :: (pad {n=n'} [] padding)
8484pad {n=S n'} (x :: xs) padding = x :: pad {n=n'} xs padding
8585
lib/Data/HVect.idr+1−1
@@ -40,7 +40,7 @@ using (k : Nat, ts : Vect Type k)
4040 class Shows (k : Nat) (ts : Vect Type k) where
4141 shows : HVect ts -> Vect String k
4242
43− instance Shows O [] where
43+ instance Shows Z [] where
4444 shows [] = []
4545
4646 instance (Show t, Shows k ts) => Shows (S k) (t::ts) where
lib/Data/SortedMap.idr+6−6
@@ -3,7 +3,7 @@ module Data.SortedMap
33-- TODO: write merge and split
44
55data Tree : Nat -> Type -> Type -> Type where
6− Leaf : k -> v -> Tree O k v
6+ Leaf : k -> v -> Tree Z k v
77 Branch2 : Tree n k v -> k -> Tree n k v -> Tree (S n) k v
88 Branch3 : Tree n k v -> k -> Tree n k v -> k -> Tree n k v -> Tree (S n) k v
99
@@ -123,7 +123,7 @@ treeInsert k v t =
123123 Right (a, b, c) => Right (Branch2 a b c)
124124
125125delType : Nat -> Type -> Type -> Type
126−delType O k v = ()
126+delType Z k v = ()
127127delType (S n) k v = Tree n k v
128128
129129treeDelete : Ord k => k -> Tree n k v -> Either (Tree n k v) (delType n k v)
@@ -132,7 +132,7 @@ treeDelete k (Leaf k' v) =
132132 Right ()
133133 else
134134 Left (Leaf k' v)
135−treeDelete {n=S O} k (Branch2 t1 k' t2) =
135+treeDelete {n=S Z} k (Branch2 t1 k' t2) =
136136 if k <= k' then
137137 case treeDelete k t1 of
138138 Left t1' => Left (Branch2 t1' k' t2)
@@ -141,7 +141,7 @@ treeDelete {n=S O} k (Branch2 t1 k' t2) =
141141 case treeDelete k t2 of
142142 Left t2' => Left (Branch2 t1 k' t2')
143143 Right () => Right t1
144−treeDelete {n=S O} k (Branch3 t1 k1 t2 k2 t3) =
144+treeDelete {n=S Z} k (Branch3 t1 k1 t2 k2 t3) =
145145 if k <= k1 then
146146 case treeDelete k t1 of
147147 Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
@@ -201,7 +201,7 @@ lookup _ Empty = Nothing
201201lookup k (M _ t) = treeLookup k t
202202
203203insert : Ord k => k -> v -> SortedMap k v -> SortedMap k v
204−insert k v Empty = M O (Leaf k v)
204+insert k v Empty = M Z (Leaf k v)
205205insert k v (M _ t) =
206206 case treeInsert k v t of
207207 Left t' => (M _ t')
@@ -209,7 +209,7 @@ insert k v (M _ t) =
209209
210210delete : Ord k => k -> SortedMap k v -> SortedMap k v
211211delete _ Empty = Empty
212−delete k (M O t) =
212+delete k (M Z t) =
213213 case treeDelete k t of
214214 Left t' => (M _ t')
215215 Right () => Empty
lib/Data/Vect.idr+1−1
@@ -14,7 +14,7 @@ data Elem : a -> Vect a k -> Type where
1414 There : {xs : Vect a k} -> Elem x xs -> Elem x (y::xs)
1515
1616findElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic
17−findElem O ctxt goal = Refine "Here" `Seq` Solve
17+findElem Z ctxt goal = Refine "Here" `Seq` Solve
1818findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))
1919
2020replaceElem : (xs : Vect t k) -> Elem x xs -> (y : t) -> (ys : Vect t k ** Elem y ys)
lib/Data/ZZ.idr+6−6
@@ -24,17 +24,17 @@ instance Show ZZ where
2424 show (NegS n) = "-" ++ show (S n)
2525
2626negZ : ZZ -> ZZ
27−negZ (Pos O) = Pos O
27+negZ (Pos Z) = Pos Z
2828negZ (Pos (S n)) = NegS n
2929negZ (NegS n) = Pos (S n)
3030
3131negNat : Nat -> ZZ
32−negNat O = Pos O
32+negNat Z = Pos Z
3333negNat (S n) = NegS n
3434
3535minusNatZ : Nat -> Nat -> ZZ
36−minusNatZ n O = Pos n
37−minusNatZ O (S m) = NegS m
36+minusNatZ n Z = Pos n
37+minusNatZ Z (S m) = NegS m
3838minusNatZ (S n) (S m) = minusNatZ n m
3939
4040plusZ : ZZ -> ZZ -> ZZ
@@ -101,9 +101,9 @@ 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 O) = refl
104+doubleNegElim (Pos Z) = refl
105105doubleNegElim (Pos (S n)) = refl
106−doubleNegElim (NegS O) = refl
106+doubleNegElim (NegS Z) = refl
107107doubleNegElim (NegS (S n)) = refl
108108
109109-- Injectivity
lib/Decidable/Equality.idr+4−4
@@ -41,13 +41,13 @@ instance DecEq Bool where
4141-- Nat
4242--------------------------------------------------------------------------------
4343
44−total OnotS : O = S n -> _|_
44+total OnotS : Z = S n -> _|_
4545OnotS refl impossible
4646
4747instance DecEq Nat where
48− decEq O O = Yes refl
49− decEq O (S _) = No OnotS
50− decEq (S _) O = No (negEqSym OnotS)
48+ decEq Z Z = Yes refl
49+ decEq Z (S _) = No OnotS
50+ decEq (S _) Z = No (negEqSym OnotS)
5151 decEq (S n) (S m) with (decEq n m)
5252 | Yes p = Yes $ cong p
5353 | No p = No $ \h : (S n = S m) => p $ succInjective n m h
lib/Decidable/Order.idr+3−3
@@ -55,7 +55,7 @@ NatLTEIsAntisymmetric n m (nLTESm _) (nLTESm _) impossible
5555instance Poset Nat NatLTE where
5656 antisymmetric = NatLTEIsAntisymmetric
5757
58−total zeroNeverGreater : {n : Nat} -> NatLTE (S n) O -> _|_
58+total zeroNeverGreater : {n : Nat} -> NatLTE (S n) Z -> _|_
5959zeroNeverGreater {n} (nLTESm _) impossible
6060zeroNeverGreater {n} nEqn impossible
6161
@@ -66,8 +66,8 @@ nGTSm {n} {m} disprf (nEqn) impossible
6666
6767total
6868decideNatLTE : (n : Nat) -> (m : Nat) -> Dec (NatLTE n m)
69−decideNatLTE O O = Yes nEqn
70−decideNatLTE (S x) O = No zeroNeverGreater
69+decideNatLTE Z Z = Yes nEqn
70+decideNatLTE (S x) Z = No zeroNeverGreater
7171decideNatLTE x (S y) with (decEq x (S y))
7272 | Yes eq = rewrite eq in Yes nEqn
7373 | No _ with (decideNatLTE x y)
lib/Prelude.idr+1−1
@@ -251,7 +251,7 @@ instance Monad List where
251251%lib C "m"
252252
253253pow : (Num a) => a -> Nat -> a
254−pow x O = 1
254+pow x Z = 1
255255pow x (S n) = x * (pow x n)
256256
257257exp : Float -> Float
lib/Prelude/Fin.idr+3−3
@@ -17,7 +17,7 @@ finToNat fO a = a
1717finToNat (fS x) a = finToNat x (S a)
1818
1919instance Cast (Fin n) Nat where
20− cast x = finToNat x O
20+ cast x = finToNat x Z
2121
2222finToInt : Fin n -> Integer -> Integer
2323finToInt fO a = a
@@ -38,7 +38,7 @@ strengthen {n = S k} (fS i) with (strengthen i)
3838strengthen f = Left f
3939
4040last : Fin (S n)
41−last {n=O} = fO
41+last {n=Z} = fO
4242last {n=S _} = fS last
4343
4444total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
@@ -48,7 +48,7 @@ fSinjective refl = refl
4848-- Construct a Fin from an integer literal which must fit in the given Fin
4949
5050natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
51−natToFin O (S j) = Just fO
51+natToFin Z (S j) = Just fO
5252natToFin (S k) (S j) with (natToFin k j)
5353 | Just k' = Just (fS k')
5454 | Nothing = Nothing
lib/Prelude/Heap.idr+2−2
@@ -27,7 +27,7 @@ isEmpty Empty = True
2727isEmpty _ = False
2828
2929total size : MaxiphobicHeap a -> Nat
30−size Empty = O
30+size Empty = Z
3131size (Node s l e r) = s
3232
3333isValidHeap : Ord a => MaxiphobicHeap a -> Bool
@@ -148,7 +148,7 @@ absurdBoolDischarge p = replace {P = disjointTy} p ()
148148 disjointTy False = ()
149149 disjointTy True = _|_
150150
151−total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = O
151+total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z
152152isEmptySizeZero Empty p = refl
153153isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd
154154
lib/Prelude/List.idr+5−5
@@ -85,12 +85,12 @@ init' (x::xs) =
8585--------------------------------------------------------------------------------
8686
8787take : Nat -> List a -> List a
88−take O xs = []
88+take Z xs = []
8989take (S n) [] = []
9090take (S n) (x::xs) = x :: take n xs
9191
9292drop : Nat -> List a -> List a
93−drop O xs = xs
93+drop Z xs = xs
9494drop (S n) [] = []
9595drop (S n) (x::xs) = drop n xs
9696
@@ -127,7 +127,7 @@ repeat : a -> List a
127127repeat x = x :: lazy (repeat x)
128128
129129replicate : Nat -> a -> List a
130−replicate O x = []
130+replicate Z x = []
131131replicate (S n) x = x :: replicate n x
132132
133133--------------------------------------------------------------------------------
@@ -325,7 +325,7 @@ find p (x::xs) =
325325 find p xs
326326
327327findIndex : (a -> Bool) -> List a -> Maybe Nat
328−findIndex = findIndex' O
328+findIndex = findIndex' Z
329329 where
330330-- findIndex' : Nat -> (a -> Bool) -> List a -> Maybe Nat
331331 findIndex' cnt p [] = Nothing
@@ -336,7 +336,7 @@ findIndex = findIndex' O
336336 findIndex' (S cnt) p xs
337337
338338findIndices : (a -> Bool) -> List a -> List Nat
339−findIndices = findIndices' O
339+findIndices = findIndices' Z
340340 where
341341-- findIndices' : Nat -> (a -> Bool) -> List a -> List Nat
342342 findIndices' cnt p [] = []
lib/Prelude/Nat.idr+105−105
@@ -9,7 +9,7 @@ import Prelude.Cast
99%default total
1010
1111data Nat
12− = O
12+ = Z
1313 | S Nat
1414
1515--------------------------------------------------------------------------------
@@ -17,11 +17,11 @@ data Nat
1717--------------------------------------------------------------------------------
1818
1919total isZero : Nat -> Bool
20−isZero O = True
20+isZero Z = True
2121isZero (S n) = False
2222
2323total isSucc : Nat -> Bool
24−isSucc O = False
24+isSucc Z = False
2525isSucc (S n) = True
2626
2727--------------------------------------------------------------------------------
@@ -29,27 +29,27 @@ isSucc (S n) = True
2929--------------------------------------------------------------------------------
3030
3131total plus : Nat -> Nat -> Nat
32−plus O right = right
32+plus Z right = right
3333plus (S left) right = S (plus left right)
3434
3535total mult : Nat -> Nat -> Nat
36−mult O right = O
36+mult Z right = Z
3737mult (S left) right = plus right $ mult left right
3838
3939total minus : Nat -> Nat -> Nat
40−minus O right = O
41−minus left O = left
40+minus Z right = Z
41+minus left Z = left
4242minus (S left) (S right) = minus left right
4343
4444total power : Nat -> Nat -> Nat
45−power base O = S O
45+power base Z = S Z
4646power base (S exp) = mult base $ power base exp
4747
4848hyper : Nat -> Nat -> Nat -> Nat
49−hyper O a b = S b
50−hyper (S O) a O = a
51−hyper (S(S O)) a O = O
52−hyper n a O = S O
49+hyper Z a b = S b
50+hyper (S Z) a Z = a
51+hyper (S(S Z)) a Z = Z
52+hyper n a Z = S Z
5353hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)
5454
5555
@@ -58,7 +58,7 @@ hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)
5858--------------------------------------------------------------------------------
5959
6060data LTE : Nat -> Nat -> Type where
61− lteZero : LTE O right
61+ lteZero : LTE Z right
6262 lteSucc : LTE left right -> LTE (S left) (S right)
6363
6464total GTE : Nat -> Nat -> Type
@@ -71,8 +71,8 @@ total GT : Nat -> Nat -> Type
7171GT left right = LT right left
7272
7373total lte : Nat -> Nat -> Bool
74−lte O right = True
75−lte left O = False
74+lte Z right = True
75+lte left Z = False
7676lte (S left) (S right) = lte left right
7777
7878total gte : Nat -> Nat -> Bool
@@ -103,18 +103,18 @@ maximum left right =
103103--------------------------------------------------------------------------------
104104
105105instance Eq Nat where
106− O == O = True
106+ Z == Z = True
107107 (S l) == (S r) = l == r
108108 _ == _ = False
109109
110110instance Cast Nat Integer where
111− cast O = 0
111+ cast Z = 0
112112 cast (S k) = 1 + cast k
113113
114114instance Ord Nat where
115− compare O O = EQ
116− compare O (S k) = LT
117− compare (S k) O = GT
115+ compare Z Z = EQ
116+ compare Z (S k) = LT
117+ compare (S k) Z = GT
118118 compare (S x) (S y) = compare x y
119119
120120instance Num Nat where
@@ -128,12 +128,12 @@ instance Num Nat where
128128 where
129129 %assert_total
130130 fromInteger' : Integer -> Nat
131− fromInteger' 0 = O
131+ fromInteger' 0 = Z
132132 fromInteger' n =
133133 if (n > 0) then
134134 S (fromInteger' (n - 1))
135135 else
136− O
136+ Z
137137
138138instance Cast Integer Nat where
139139 cast = fromInteger
@@ -171,10 +171,10 @@ instance Semigroup Additive where
171171 getAdditive m => m
172172
173173instance Monoid Multiplicative where
174− neutral = getMultiplicative $ S O
174+ neutral = getMultiplicative $ S Z
175175
176176instance Monoid Additive where
177− neutral = getAdditive O
177+ neutral = getAdditive Z
178178
179179instance MeetSemilattice Nat where
180180 meet = minimum
@@ -185,14 +185,14 @@ instance JoinSemilattice Nat where
185185instance Lattice Nat where { }
186186
187187instance BoundedJoinSemilattice Nat where
188− bottom = O
188+ bottom = Z
189189
190190--------------------------------------------------------------------------------
191191-- Auxilliary notions
192192--------------------------------------------------------------------------------
193193
194194total pred : Nat -> Nat
195−pred O = O
195+pred Z = Z
196196pred (S n) = n
197197
198198--------------------------------------------------------------------------------
@@ -200,8 +200,8 @@ pred (S n) = n
200200--------------------------------------------------------------------------------
201201
202202total fib : Nat -> Nat
203−fib O = O
204−fib (S O) = S O
203+fib Z = Z
204+fib (S Z) = S Z
205205fib (S (S n)) = fib (S n) + fib n
206206
207207--------------------------------------------------------------------------------
@@ -213,11 +213,11 @@ fib (S (S n)) = fib (S n) + fib n
213213--------------------------------------------------------------------------------
214214
215215total mod : Nat -> Nat -> Nat
216−mod left O = left
216+mod left Z = left
217217mod left (S right) = mod' left left right
218218 where
219219 total mod' : Nat -> Nat -> Nat -> Nat
220− mod' O centre right = centre
220+ mod' Z centre right = centre
221221 mod' (S left) centre right =
222222 if lte centre right then
223223 centre
@@ -225,21 +225,21 @@ mod left (S right) = mod' left left right
225225 mod' left (centre - (S right)) right
226226
227227total div : Nat -> Nat -> Nat
228−div left O = S left -- div by zero
228+div left Z = S left -- div by zero
229229div left (S right) = div' left left right
230230 where
231231 total div' : Nat -> Nat -> Nat -> Nat
232− div' O centre right = O
232+ div' Z centre right = Z
233233 div' (S left) centre right =
234234 if lte centre right then
235− O
235+ Z
236236 else
237237 S (div' left (centre - (S right)) right)
238238
239239%assert_total
240240log2 : Nat -> Nat
241−log2 O = O
242−log2 (S O) = O
241+log2 Z = Z
242+log2 (S Z) = Z
243243log2 n = S (log2 (n `div` 2))
244244
245245--------------------------------------------------------------------------------
@@ -260,28 +260,28 @@ total plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
260260plusZeroLeftNeutral right = refl
261261
262262total plusZeroRightNeutral : (left : Nat) -> left + 0 = left
263−plusZeroRightNeutral O = refl
263+plusZeroRightNeutral Z = refl
264264plusZeroRightNeutral (S n) =
265265 let inductiveHypothesis = plusZeroRightNeutral n in
266266 ?plusZeroRightNeutralStepCase
267267
268268total plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
269269 S (left + right) = left + (S right)
270−plusSuccRightSucc O right = refl
270+plusSuccRightSucc Z right = refl
271271plusSuccRightSucc (S left) right =
272272 let inductiveHypothesis = plusSuccRightSucc left right in
273273 ?plusSuccRightSuccStepCase
274274
275275total plusCommutative : (left : Nat) -> (right : Nat) ->
276276 left + right = right + left
277−plusCommutative O right = ?plusCommutativeBaseCase
277+plusCommutative Z right = ?plusCommutativeBaseCase
278278plusCommutative (S left) right =
279279 let inductiveHypothesis = plusCommutative left right in
280280 ?plusCommutativeStepCase
281281
282282total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
283283 left + (centre + right) = (left + centre) + right
284−plusAssociative O centre right = refl
284+plusAssociative Z centre right = refl
285285plusAssociative (S left) centre right =
286286 let inductiveHypothesis = plusAssociative left centre right in
287287 ?plusAssociativeStepCase
@@ -299,38 +299,38 @@ plusOneSucc n = refl
299299
300300total plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
301301 (p : left + right = left + right') -> right = right'
302−plusLeftCancel O right right' p = ?plusLeftCancelBaseCase
302+plusLeftCancel Z right right' p = ?plusLeftCancelBaseCase
303303plusLeftCancel (S left) right right' p =
304304 let inductiveHypothesis = plusLeftCancel left right right' in
305305 ?plusLeftCancelStepCase
306306
307307total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
308308 (p : left + right = left' + right) -> left = left'
309−plusRightCancel left left' O p = ?plusRightCancelBaseCase
309+plusRightCancel left left' Z p = ?plusRightCancelBaseCase
310310plusRightCancel left left' (S right) p =
311311 let inductiveHypothesis = plusRightCancel left left' right in
312312 ?plusRightCancelStepCase
313313
314314total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
315− (p : left + right = left) -> right = O
316−plusLeftLeftRightZero O right p = ?plusLeftLeftRightZeroBaseCase
315+ (p : left + right = left) -> right = Z
316+plusLeftLeftRightZero Z right p = ?plusLeftLeftRightZeroBaseCase
317317plusLeftLeftRightZero (S left) right p =
318318 let inductiveHypothesis = plusLeftLeftRightZero left right in
319319 ?plusLeftLeftRightZeroStepCase
320320
321321-- Mult
322−total multZeroLeftZero : (right : Nat) -> O * right = O
322+total multZeroLeftZero : (right : Nat) -> Z * right = Z
323323multZeroLeftZero right = refl
324324
325−total multZeroRightZero : (left : Nat) -> left * O = O
326−multZeroRightZero O = refl
325+total multZeroRightZero : (left : Nat) -> left * Z = Z
326+multZeroRightZero Z = refl
327327multZeroRightZero (S left) =
328328 let inductiveHypothesis = multZeroRightZero left in
329329 ?multZeroRightZeroStepCase
330330
331331total multRightSuccPlus : (left : Nat) -> (right : Nat) ->
332332 left * (S right) = left + (left * right)
333−multRightSuccPlus O right = refl
333+multRightSuccPlus Z right = refl
334334multRightSuccPlus (S left) right =
335335 let inductiveHypothesis = multRightSuccPlus left right in
336336 ?multRightSuccPlusStepCase
@@ -341,40 +341,40 @@ multLeftSuccPlus left right = refl
341341
342342total multCommutative : (left : Nat) -> (right : Nat) ->
343343 left * right = right * left
344−multCommutative O right = ?multCommutativeBaseCase
344+multCommutative Z right = ?multCommutativeBaseCase
345345multCommutative (S left) right =
346346 let inductiveHypothesis = multCommutative left right in
347347 ?multCommutativeStepCase
348348
349349total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
350350 left * (centre + right) = (left * centre) + (left * right)
351−multDistributesOverPlusRight O centre right = refl
351+multDistributesOverPlusRight Z centre right = refl
352352multDistributesOverPlusRight (S left) centre right =
353353 let inductiveHypothesis = multDistributesOverPlusRight left centre right in
354354 ?multDistributesOverPlusRightStepCase
355355
356356total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
357357 (left + centre) * right = (left * right) + (centre * right)
358−multDistributesOverPlusLeft O centre right = refl
358+multDistributesOverPlusLeft Z centre right = refl
359359multDistributesOverPlusLeft (S left) centre right =
360360 let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
361361 ?multDistributesOverPlusLeftStepCase
362362
363363total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
364364 left * (centre * right) = (left * centre) * right
365−multAssociative O centre right = refl
365+multAssociative Z centre right = refl
366366multAssociative (S left) centre right =
367367 let inductiveHypothesis = multAssociative left centre right in
368368 ?multAssociativeStepCase
369369
370370total multOneLeftNeutral : (right : Nat) -> 1 * right = right
371−multOneLeftNeutral O = refl
371+multOneLeftNeutral Z = refl
372372multOneLeftNeutral (S right) =
373373 let inductiveHypothesis = multOneLeftNeutral right in
374374 ?multOneLeftNeutralStepCase
375375
376376total multOneRightNeutral : (left : Nat) -> left * 1 = left
377−multOneRightNeutral O = refl
377+multOneRightNeutral Z = refl
378378multOneRightNeutral (S left) =
379379 let inductiveHypothesis = multOneRightNeutral left in
380380 ?multOneRightNeutralStepCase
@@ -384,51 +384,51 @@ total minusSuccSucc : (left : Nat) -> (right : Nat) ->
384384 (S left) - (S right) = left - right
385385minusSuccSucc left right = refl
386386
387−total minusZeroLeft : (right : Nat) -> 0 - right = O
387+total minusZeroLeft : (right : Nat) -> 0 - right = Z
388388minusZeroLeft right = refl
389389
390390total minusZeroRight : (left : Nat) -> left - 0 = left
391−minusZeroRight O = refl
391+minusZeroRight Z = refl
392392minusZeroRight (S left) = refl
393393
394−total minusZeroN : (n : Nat) -> O = n - n
395−minusZeroN O = refl
394+total minusZeroN : (n : Nat) -> Z = n - n
395+minusZeroN Z = refl
396396minusZeroN (S n) = minusZeroN n
397397
398−total minusOneSuccN : (n : Nat) -> S O = (S n) - n
399−minusOneSuccN O = refl
398+total minusOneSuccN : (n : Nat) -> S Z = (S n) - n
399+minusOneSuccN Z = refl
400400minusOneSuccN (S n) = minusOneSuccN n
401401
402402total minusSuccOne : (n : Nat) -> S n - 1 = n
403−minusSuccOne O = refl
403+minusSuccOne Z = refl
404404minusSuccOne (S n) = refl
405405
406−total minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = O
407−minusPlusZero O m = refl
406+total minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = Z
407+minusPlusZero Z m = refl
408408minusPlusZero (S n) m = minusPlusZero n m
409409
410410total minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
411411 left - centre - right = left - (centre + right)
412−minusMinusMinusPlus O O right = refl
413−minusMinusMinusPlus (S left) O right = refl
414−minusMinusMinusPlus O (S centre) right = refl
412+minusMinusMinusPlus Z Z right = refl
413+minusMinusMinusPlus (S left) Z right = refl
414+minusMinusMinusPlus Z (S centre) right = refl
415415minusMinusMinusPlus (S left) (S centre) right =
416416 let inductiveHypothesis = minusMinusMinusPlus left centre right in
417417 ?minusMinusMinusPlusStepCase
418418
419419total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
420420 (left + right) - (left + right') = right - right'
421−plusMinusLeftCancel O right right' = refl
421+plusMinusLeftCancel Z right right' = refl
422422plusMinusLeftCancel (S left) right right' =
423423 let inductiveHypothesis = plusMinusLeftCancel left right right' in
424424 ?plusMinusLeftCancelStepCase
425425
426426total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
427427 (left - centre) * right = (left * right) - (centre * right)
428−multDistributesOverMinusLeft O O right = refl
429−multDistributesOverMinusLeft (S left) O right =
428+multDistributesOverMinusLeft Z Z right = refl
429+multDistributesOverMinusLeft (S left) Z right =
430430 ?multDistributesOverMinusLeftBaseCase
431−multDistributesOverMinusLeft O (S centre) right = refl
431+multDistributesOverMinusLeft Z (S centre) right = refl
432432multDistributesOverMinusLeft (S left) (S centre) right =
433433 let inductiveHypothesis = multDistributesOverMinusLeft left centre right in
434434 ?multDistributesOverMinusLeftStepCase
@@ -445,35 +445,35 @@ powerSuccPowerLeft base exp = refl
445445
446446total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
447447 (power base exp) * (power base exp') = power base (exp + exp')
448−multPowerPowerPlus base O exp' = ?multPowerPowerPlusBaseCase
448+multPowerPowerPlus base Z exp' = ?multPowerPowerPlusBaseCase
449449multPowerPowerPlus base (S exp) exp' =
450450 let inductiveHypothesis = multPowerPowerPlus base exp exp' in
451451 ?multPowerPowerPlusStepCase
452452
453−total powerZeroOne : (base : Nat) -> power base 0 = S O
453+total powerZeroOne : (base : Nat) -> power base 0 = S Z
454454powerZeroOne base = refl
455455
456456total powerOneNeutral : (base : Nat) -> power base 1 = base
457−powerOneNeutral O = refl
457+powerOneNeutral Z = refl
458458powerOneNeutral (S base) =
459459 let inductiveHypothesis = powerOneNeutral base in
460460 ?powerOneNeutralStepCase
461461
462−total powerOneSuccOne : (exp : Nat) -> power 1 exp = S O
463−powerOneSuccOne O = refl
462+total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z
463+powerOneSuccOne Z = refl
464464powerOneSuccOne (S exp) =
465465 let inductiveHypothesis = powerOneSuccOne exp in
466466 ?powerOneSuccOneStepCase
467467
468468total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
469−powerSuccSuccMult O = refl
469+powerSuccSuccMult Z = refl
470470powerSuccSuccMult (S base) =
471471 let inductiveHypothesis = powerSuccSuccMult base in
472472 ?powerSuccSuccMultStepCase
473473
474474total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
475475 power (power base exp) exp' = power base (exp * exp')
476−powerPowerMultPower base exp O = ?powerPowerMultPowerBaseCase
476+powerPowerMultPower base exp Z = ?powerPowerMultPowerBaseCase
477477powerPowerMultPower base exp (S exp') =
478478 let inductiveHypothesis = powerPowerMultPower base exp exp' in
479479 ?powerPowerMultPowerStepCase
@@ -484,9 +484,9 @@ predSucc n = refl
484484
485485total minusSuccPred : (left : Nat) -> (right : Nat) ->
486486 left - (S right) = pred (left - right)
487−minusSuccPred O right = refl
488−minusSuccPred (S left) O =
489− let inductiveHypothesis = minusSuccPred left O in
487+minusSuccPred Z right = refl
488+minusSuccPred (S left) Z =
489+ let inductiveHypothesis = minusSuccPred left Z in
490490 ?minusSuccPredStepCase
491491minusSuccPred (S left) (S right) =
492492 let inductiveHypothesis = minusSuccPred left right in
@@ -520,69 +520,69 @@ boolElimMultMultRight False right t f = refl
520520
521521-- Orders
522522total lteNTrue : (n : Nat) -> lte n n = True
523−lteNTrue O = refl
523+lteNTrue Z = refl
524524lteNTrue (S n) = lteNTrue n
525525
526−total lteSuccZeroFalse : (n : Nat) -> lte (S n) O = False
527−lteSuccZeroFalse O = refl
526+total lteSuccZeroFalse : (n : Nat) -> lte (S n) Z = False
527+lteSuccZeroFalse Z = refl
528528lteSuccZeroFalse (S n) = refl
529529
530530-- Minimum and maximum
531−total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = O
532−minimumZeroZeroRight O = refl
531+total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z
532+minimumZeroZeroRight Z = refl
533533minimumZeroZeroRight (S right) = minimumZeroZeroRight right
534534
535−total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = O
536−minimumZeroZeroLeft O = refl
535+total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
536+minimumZeroZeroLeft Z = refl
537537minimumZeroZeroLeft (S left) = refl
538538
539539total minimumSuccSucc : (left : Nat) -> (right : Nat) ->
540540 minimum (S left) (S right) = S (minimum left right)
541−minimumSuccSucc O O = refl
542−minimumSuccSucc (S left) O = refl
543−minimumSuccSucc O (S right) = refl
541+minimumSuccSucc Z Z = refl
542+minimumSuccSucc (S left) Z = refl
543+minimumSuccSucc Z (S right) = refl
544544minimumSuccSucc (S left) (S right) =
545545 let inductiveHypothesis = minimumSuccSucc left right in
546546 ?minimumSuccSuccStepCase
547547
548548total minimumCommutative : (left : Nat) -> (right : Nat) ->
549549 minimum left right = minimum right left
550−minimumCommutative O O = refl
551−minimumCommutative O (S right) = refl
552−minimumCommutative (S left) O = refl
550+minimumCommutative Z Z = refl
551+minimumCommutative Z (S right) = refl
552+minimumCommutative (S left) Z = refl
553553minimumCommutative (S left) (S right) =
554554 let inductiveHypothesis = minimumCommutative left right in
555555 ?minimumCommutativeStepCase
556556
557−total maximumZeroNRight : (right : Nat) -> maximum O right = right
558−maximumZeroNRight O = refl
557+total maximumZeroNRight : (right : Nat) -> maximum Z right = right
558+maximumZeroNRight Z = refl
559559maximumZeroNRight (S right) = refl
560560
561−total maximumZeroNLeft : (left : Nat) -> maximum left O = left
562−maximumZeroNLeft O = refl
561+total maximumZeroNLeft : (left : Nat) -> maximum left Z = left
562+maximumZeroNLeft Z = refl
563563maximumZeroNLeft (S left) = refl
564564
565565total maximumSuccSucc : (left : Nat) -> (right : Nat) ->
566566 S (maximum left right) = maximum (S left) (S right)
567−maximumSuccSucc O O = refl
568−maximumSuccSucc (S left) O = refl
569−maximumSuccSucc O (S right) = refl
567+maximumSuccSucc Z Z = refl
568+maximumSuccSucc (S left) Z = refl
569+maximumSuccSucc Z (S right) = refl
570570maximumSuccSucc (S left) (S right) =
571571 let inductiveHypothesis = maximumSuccSucc left right in
572572 ?maximumSuccSuccStepCase
573573
574574total maximumCommutative : (left : Nat) -> (right : Nat) ->
575575 maximum left right = maximum right left
576−maximumCommutative O O = refl
577−maximumCommutative (S left) O = refl
578−maximumCommutative O (S right) = refl
576+maximumCommutative Z Z = refl
577+maximumCommutative (S left) Z = refl
578+maximumCommutative Z (S right) = refl
579579maximumCommutative (S left) (S right) =
580580 let inductiveHypothesis = maximumCommutative left right in
581581 ?maximumCommutativeStepCase
582582
583583-- div and mod
584−total modZeroZero : (n : Nat) -> mod 0 n = O
585−modZeroZero O = refl
584+total modZeroZero : (n : Nat) -> mod 0 n = Z
585+modZeroZero Z = refl
586586modZeroZero (S n) = refl
587587
588588--------------------------------------------------------------------------------
@@ -613,7 +613,7 @@ powerSuccSuccMultStepCase = proof {
613613powerOneSuccOneStepCase = proof {
614614 intros;
615615 rewrite inductiveHypothesis;
616− rewrite sym (plusZeroRightNeutral (power (S O) exp));
616+ rewrite sym (plusZeroRightNeutral (power (S Z) exp));
617617 trivial;
618618}
619619
lib/Prelude/Vect.idr+3−3
@@ -10,7 +10,7 @@ import Prelude.Nat
1010infixr 7 ::
1111
1212data Vect : Type -> Nat -> Type where
13− Nil : Vect a O
13+ Nil : Vect a Z
1414 (::) : a -> Vect a n -> Vect a (S n)
1515
1616--------------------------------------------------------------------------------
@@ -81,7 +81,7 @@ fromList (x::xs) = x :: fromList xs
8181(++) (x::xs) ys = x :: xs ++ ys
8282
8383replicate : (n : Nat) -> a -> Vect a n
84−replicate O x = []
84+replicate Z x = []
8585replicate (S k) x = x :: replicate k x
8686
8787--------------------------------------------------------------------------------
@@ -322,7 +322,7 @@ range =
322322 reverse range_
323323 where
324324 range_ : Vect (Fin n) n
325− range_ {n=O} = Nil
325+ range_ {n=Z} = Nil
326326 range_ {n=(S _)} = last :: map weaken range_
327327
328328--------------------------------------------------------------------------------
lib/Uninhabited.idr+2−2
@@ -3,10 +3,10 @@ module Uninhabited
33class Uninhabited t where
44 total uninhabited : t -> _|_
55
6−instance Uninhabited (Fin O) where
6+instance Uninhabited (Fin Z) where
77 uninhabited fO impossible
88 uninhabited (fS f) impossible
99
10−instance Uninhabited (O = S n) where
10+instance Uninhabited (Z = S n) where
1111 uninhabited refl impossible
1212
samples/binary.idr+2−2
@@ -11,7 +11,7 @@ instance Show (Bit n) where
1111infixl 5 #
1212
1313data Binary : (width : Nat) -> (value : Nat) -> Type where
14− zero : Binary O O
14+ zero : Binary Z Z
1515 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
1616
1717instance Show (Binary w k) where
@@ -83,7 +83,7 @@ main.adc_lemma_2 = proof {
8383 rewrite sym (plusAssociative x v v1);
8484 rewrite sym (plusCommutative (plus (plus x v) v1) v1);
8585 rewrite plusZeroRightNeutral (plus (plus x v) v1);
86− rewrite sym (plusAssociative (plus x v) v1 (plus (plus (plus x v) v1) O));
86+ rewrite sym (plusAssociative (plus x v) v1 (plus (plus (plus x v) v1) Z));
8787 trivial;
8888}
8989
src/IRTS/Compiler.hs+3−3
@@ -237,7 +237,7 @@ instance ToIR (TT Name) where
237237 where mkUnused u i [] = []
238238 mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs
239239 | otherwise = x : mkUnused u (i + 1) xs
240−-- ir' env (P _ (NS (UN "O") ["Nat", "Prelude"]) _)
240+-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)
241241-- = return $ LConst (BI 0)
242242 ir' env (P _ n _) = return $ LV (Glob n)
243243 ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))
@@ -331,7 +331,7 @@ mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
331331mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
332332mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
333333
334−zname = NS (UN "O") ["Nat","Prelude"]
334+zname = NS (UN "Z") ["Nat","Prelude"]
335335sname = NS (UN "S") ["Nat","Prelude"]
336336
337337instance ToIR ([Name], SC) where
@@ -351,7 +351,7 @@ instance ToIR SC where
351351 return $ LCase (LV (Glob n)) alts'
352352 ir' ImpossibleCase = return LNothing
353353
354− -- special cases for O and S
354+ -- special cases for Z and S
355355 -- Needs rethink: projections make this fail
356356-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
357357-- = mkIRAlt n (ConstCase (BI 0) rhs)
src/Idris/AbsSyntaxTree.hs+2−2
@@ -1128,10 +1128,10 @@ showImp impl tm = se 10 tm where
11281128 xs -> "[" ++ intercalate "," (map (se p) xs) ++ "]"
11291129 slist _ _ = Nothing
11301130
1131− -- since Prelude is always imported, S & O are unqualified iff they're the
1131+ -- since Prelude is always imported, S & Z are unqualified iff they're the
11321132 -- Nat ones.
11331133 snat p (PRef _ o)
1134− | show o == (natns++"O") || show o == "O" = Just 0
1134+ | show o == (natns++"Z") || show o == "Z" = Just 0
11351135 snat p (PApp _ s [PExp {getTm=n}])
11361136 | show s == (natns++"S") || show s == "S",
11371137 Just n' <- snat p n
src/Idris/Transforms.hs+1−1
@@ -39,7 +39,7 @@ instance Transform CaseAlt where
3939
4040natTrans = [TermTrans zero, TermTrans suc, CaseTrans natcase]
4141
42−zname = NS (UN "O") ["Nat","Prelude"]
42+zname = NS (UN "Z") ["Nat","Prelude"]
4343sname = NS (UN "S") ["Nat","Prelude"]
4444
4545zero :: TT Name -> TT Name
test/reg001/reg001.idr+1−1
@@ -8,4 +8,4 @@ data Imp : Type where
88 MkImp : {any : Type} -> any -> Imp
99
1010testVal : Imp
11−testVal = MkImp (apply id O)
11+testVal = MkImp (apply id Z)
test/reg004/reg004.idr+2−2
@@ -3,12 +3,12 @@ module Main
33h : Bool -> Nat
44h False = r1 where
55 r : Nat
6− r = S O
6+ r = S Z
77 r1 : Nat
88 r1 = r
99h True = r2 where
1010 r : Nat
11− r = O
11+ r = Z
1212 r2 : Nat
1313 r2 = r
1414
test/reg005/reg005.idr+3−3
@@ -1,7 +1,7 @@
11module Main
22
33rep : (n : Nat) -> Char -> Vect Char n
4−rep O x = []
4+rep Z x = []
55rep (S k) x = x :: rep k x
66
77data RLE : Vect Char n -> Type where
@@ -18,12 +18,12 @@ eq x y = if x == y then Just ?eqCharOK else Nothing
1818rle : (xs : Vect Char n) -> RLE xs
1919rle [] = REnd
2020rle (x :: xs) with (rle xs)
21− rle (x :: Vect.Nil) | REnd = RChar O x REnd
21+ rle (x :: Vect.Nil) | REnd = RChar Z x REnd
2222 rle (x :: rep (S n) yvar ++ ys) | RChar n yvar rs with (eq x yvar)
2323 rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just refl
2424 = RChar (S n) x rs
2525 rle (x :: rep (S n) y ++ ys) | RChar n y rs | Nothing
26− = RChar O x (RChar n y rs)
26+ = RChar Z x (RChar n y rs)
2727
2828compress : Vect Char n -> String
2929compress xs with (rle xs)
test/reg006/reg006.idr+1−1
@@ -3,7 +3,7 @@ module RBTree
33data Colour = Red | Black
44
55data RBTree : Type -> Type -> Nat -> Colour -> Type where
6− Leaf : RBTree k v O Black
6+ Leaf : RBTree k v Z Black
77 RedBranch : k -> v -> RBTree k v n Black -> RBTree k v n Black -> RBTree k v n Red
88 BlackBranch : k -> v -> RBTree k v n x -> RBTree k v n y -> RBTree k v (S n) Black
99
test/reg008/reg008.idr+3−3
@@ -6,9 +6,9 @@ data Cmp : Nat -> Nat -> Type where
66 cmpGT : (x : _) -> Cmp (y + S x) y
77
88total cmp : (x, y : Nat) -> Cmp x y
9−cmp O O = cmpEQ
10−cmp O (S k) = cmpLT _
11−cmp (S k) O = cmpGT _
9+cmp Z Z = cmpEQ
10+cmp Z (S k) = cmpLT _
11+cmp (S k) Z = cmpGT _
1212cmp (S x) (S y) with (cmp x y)
1313 cmp (S x) (S (x + (S k))) | cmpLT k = cmpLT k
1414 cmp (S x) (S x) | cmpEQ = cmpEQ
test/reg009/reg009.lidr+1−1
@@ -6,7 +6,7 @@
66> filterTagP : (p : alpha -> Bool) ->
77> (as : Vect alpha n) ->
88> so (isAnyBy p (n ** as)) ->
9−> (m : Nat ** (Vect (a : alpha ** so (p a)) m, so (m > O)))
9+> (m : Nat ** (Vect (a : alpha ** so (p a)) m, so (m > Z)))
1010> filterTagP {n = S m} p (a :: as) q with (p a)
1111> | True = (_
1212> **
test/reg010/reg010.idr+1−1
@@ -1,5 +1,5 @@
11module usubst
22
33total unsafeSubst : (P : a -> Type) -> (x : a) -> (y : a) -> P x -> P y
4−unsafeSubst P x y px with (O)
4+unsafeSubst P x y px with (Z)
55 unsafeSubst P x x px | _ = px
test/reg011/reg011.idr+2−2
@@ -1,9 +1,9 @@
11vfoldl : (P : Nat -> Type) ->
2− ((x : Nat) -> P x -> a -> P (S x)) -> P O
2+ ((x : Nat) -> P x -> a -> P (S x)) -> P Z
33 -> Vect a m -> P m
44-- vfoldl P cons nil []
55-- = nil
66vfoldl P cons nil (x :: xs)
7− = vfoldl (\k => P (S k)) (\ n => cons (S n)) (cons O nil x) xs
7+ = vfoldl (\k => P (S k)) (\ n => cons (S n)) (cons Z nil x) xs
88-- vfoldl P cons nil (x :: xs)
99-- = vfoldl (\n => P (S n)) (\ n => cons _) (cons _ nil x) xs
test/reg018/reg018b.idr+3−3
@@ -2,13 +2,13 @@ module A
22
33%default total
44
5−codata B = O B | I B
5+codata B = Z B | I B
66
77showB : B -> String
88showB (I x) = "I" ++ showB x
9−showB (O x) = "O" ++ showB x
9+showB (Z x) = "Z" ++ showB x
1010
1111instance Show B where show = showB
1212
1313os : B
14−os = O os
14+os = Z os
test/reg018/reg018c.idr+1−1
@@ -9,7 +9,7 @@ codata InfStream a = (::) a (InfStream a)
99-- natFromStream n = (::) n (natFromStream (S n))
1010
1111take : (n: Nat) -> InfStream a -> Vect a n
12−take O _ = []
12+take Z _ = []
1313take (S n) (x :: xs) = x :: take n xs
1414
1515hdtl : InfStream a -> (a, InfStream a)
test/reg018/reg018d.idr+1−1
@@ -2,7 +2,7 @@ module Main
22
33total
44pull : Fin (S n) -> Vect a (S n) -> (a, Vect a n)
5−pull {n=O} _ (x :: xs) = (x, xs)
5+pull {n=Z} _ (x :: xs) = (x, xs)
66-- pull {n=S q} fO (Vect.(::) {n=S _} x xs) = (x, xs)
77pull {n=S _} (fS n) (x :: xs) =
88 let (v, vs) = pull n xs in
test/test005/test005.idr+1−1
@@ -8,7 +8,7 @@ tlist = [1, 2, 3, 4, 5]
88
99main : IO ()
1010main = do print (abs (-8))
11− print (abs (S O))
11+ print (abs (S Z))
1212 print (span isAlpha tstr)
1313 print (break isDigit tstr)
1414 print (span (\x => x < 3) tlist)
test/test006/test006.idr+3−3
@@ -5,14 +5,14 @@ data Parity : Nat -> Type where
55 odd : Parity (S (n + n))
66
77parity : (n:Nat) -> Parity n
8−parity O = even {n=O}
9−parity (S O) = odd {n=O}
8+parity Z = even {n=Z}
9+parity (S Z) = odd {n=Z}
1010parity (S (S k)) with (parity k)
1111 parity (S (S (j + j))) | (even {n = j}) ?= even {n=S j}
1212 parity (S (S (S (j + j)))) | (odd {n = j}) ?= odd {n=S j}
1313
1414natToBin : Nat -> List Bool
15−natToBin O = Nil
15+natToBin Z = Nil
1616natToBin k with (parity k)
1717 natToBin (j + j) | even {n = j} = False :: natToBin j
1818 natToBin (S (j + j)) | odd {n = j} = True :: natToBin j
test/test015/Parity.idr+2−2
@@ -5,8 +5,8 @@ data Parity : Nat -> Type where
55 odd : Parity (S (n + n))
66
77parity : (n:Nat) -> Parity n
8−parity O = even {n=O}
9−parity (S O) = odd {n=O}
8+parity Z = even {n=Z}
9+parity (S Z) = odd {n=Z}
1010parity (S (S k)) with (parity k)
1111 parity (S (S (j + j))) | even ?= even {n=S j}
1212 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
test/test015/test015.idr+6−6
@@ -4,8 +4,8 @@ import Parity
44import System
55
66data Bit : Nat -> Type where
7− b0 : Bit O
8− b1 : Bit (S O)
7+ b0 : Bit Z
8+ b1 : Bit (S Z)
99
1010instance Show (Bit n) where
1111 show = show' where
@@ -16,7 +16,7 @@ instance Show (Bit n) where
1616infixl 5 #
1717
1818data Binary : (width : Nat) -> (value : Nat) -> Type where
19− zero : Binary O O
19+ zero : Binary Z Z
2020 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
2121
2222instance Show (Binary w k) where
@@ -29,9 +29,9 @@ pad (num # x) = pad num # x
2929
3030natToBin : (width : Nat) -> (n : Nat) ->
3131 Maybe (Binary width n)
32−natToBin O (S k) = Nothing
33−natToBin O O = Just zero
34−natToBin (S k) O = do x <- natToBin k O
32+natToBin Z (S k) = Nothing
33+natToBin Z Z = Just zero
34+natToBin (S k) Z = do x <- natToBin k Z
3535 Just (pad x)
3636natToBin (S w) (S k) with (parity k)
3737 natToBin (S w) (S (plus j j)) | even = do jbin <- natToBin w j
test/test016/test016.idr+1−1
@@ -8,7 +8,7 @@ countFrom : Int -> Stream Int
88countFrom x = x :: countFrom (x + 1)
99
1010take : Nat -> Stream a -> List a
11−take O _ = []
11+take Z _ = []
1212take (S n) (x :: xs) = x :: take n xs
1313take n [] = []
1414
test/test017/test017.idr+16−16
@@ -5,8 +5,8 @@ module scg
55data Ord = Zero | Suc Ord | Sup (Nat -> Ord)
66
77natElim : (n : Nat) -> (P : Nat -> Type) ->
8− (P O) -> ((n : Nat) -> (P n) -> (P (S n))) -> (P n)
9−natElim O P mO mS = mO
8+ (P Z) -> ((n : Nat) -> (P n) -> (P (S n))) -> (P n)
9+natElim Z P mO mS = mO
1010natElim (S k) P mO mS = mS k (natElim k P mO mS)
1111
1212ordElim : (x : Ord) ->
@@ -23,10 +23,10 @@ ordElim (Sup f) P mZ mSuc mSup =
2323myplus' : Nat -> Nat -> Nat
2424myplus : Nat -> Nat -> Nat
2525
26−myplus O y = y
26+myplus Z y = y
2727myplus (S k) y = S (myplus' k y)
2828
29−myplus' O y = y
29+myplus' Z y = y
3030myplus' (S k) y = S (myplus y k)
3131
3232mnubBy : (a -> a -> Bool) -> List a -> List a
@@ -46,23 +46,23 @@ vtrans [] _ = []
4646vtrans (x :: xs) ys = x :: vtrans ys ys
4747
4848even : Nat -> Bool
49−even O = True
49+even Z = True
5050even (S k) = odd k
5151 where
5252 odd : Nat -> Bool
53− odd O = False
53+ odd Z = False
5454 odd (S k) = even k
5555
5656ack : Nat -> Nat -> Nat
57−ack O n = S n
58−ack (S m) O = ack m (S O)
57+ack Z n = S n
58+ack (S m) Z = ack m (S Z)
5959ack (S m) (S n) = ack m (ack (S m) n)
6060
6161data Bin = eps | c0 Bin | c1 Bin
6262
6363foo : Bin -> Nat
64−foo eps = O
65−foo (c0 eps) = O
64+foo eps = Z
65+foo (c0 eps) = Z
6666foo (c0 (c1 x)) = S (foo (c1 x))
6767foo (c0 (c0 x)) = foo (c0 x)
6868foo (c1 x) = S (foo x)
@@ -70,19 +70,19 @@ foo (c1 x) = S (foo x)
7070bar : Nat -> Nat -> Nat
7171bar x y = mp x y where
7272 mp : Nat -> Nat -> Nat
73− mp O y = y
73+ mp Z y = y
7474 mp (S k) y = S (bar k y)
7575
7676total mfib : Nat -> Nat
77−mfib O = O
78−mfib (S O) = S O
77+mfib Z = Z
78+mfib (S Z) = S Z
7979mfib (S (S n)) = mfib (S n) + mfib n
8080
8181maxCommutative : (left : Nat) -> (right : Nat) ->
8282 maximum left right = maximum right left
83−maxCommutative O O = refl
84−maxCommutative (S left) O = refl
85−maxCommutative O (S right) = refl
83+maxCommutative Z Z = refl
84+maxCommutative (S left) Z = refl
85+maxCommutative Z (S right) = refl
8686maxCommutative (S left) (S right) =
8787 let inductiveHypothesis = maxCommutative left right in
8888 ?maxCommutativeStepCase
test/test019/test019.lidr+1−1
@@ -1,7 +1,7 @@
11> module Main
22
33> ifTrue : so True -> Nat
4−> ifTrue oh = S O
4+> ifTrue oh = S Z
55
66> ifFalse : so False -> Nat
77> ifFalse oh impossible
test/test025/test025.idr+2−2
@@ -21,9 +21,9 @@ testMemory = do Src :- allocate 5
2121 Dst :- initialize (prim__truncInt_B8 1) 2 oh
2222 move 2 2 3 oh oh
2323 Src :- free
24− end <- Dst :- peek 4 (S O) oh
24+ end <- Dst :- peek 4 (S Z) oh
2525 Dst :- poke 4 (sub1 end) oh
26− res <- Dst :- peek 1 (S(S(S(S O)))) oh
26+ res <- Dst :- peek 1 (S(S(S(S Z)))) oh
2727 Dst :- free
2828 return (map (prim__zextB8_Int) res)
2929
tutorial/classes.tex+8−8
@@ -43,10 +43,10 @@ could be defined as:
4343\begin{SaveVerbatim}{shownat}
4444
4545instance Show Nat where
46− show O = "O"
46+ show Z = "Z"
4747 show (S k) = "s" ++ show k
4848
49−Idris> show (S (S (S O)))
49+Idris> show (S (S (S Z)))
5050"sssO" : String
5151
5252\end{SaveVerbatim}
@@ -101,10 +101,10 @@ For example, for an instance of \texttt{Eq} for \texttt{Nat}:
101101\begin{SaveVerbatim}{eqnat}
102102
103103instance Eq Nat where
104− O == O = True
104+ Z == Z = True
105105 (S x) == (S y) = x == y
106− O == (S y) = False
107− (S x) == O = False
106+ Z == (S y) = False
107+ (S x) == Z = False
108108
109109 x /= y = not (x == y)
110110
@@ -498,9 +498,9 @@ be \remph{named} as follows:
498498\begin{SaveVerbatim}{myord}
499499
500500instance [myord] Ord Nat where
501− compare O (S n) = GT
502− compare (S n) O = LT
503− compare O O = EQ
501+ compare Z (S n) = GT
502+ compare (S n) Z = LT
503+ compare Z Z = EQ
504504 compare (S x) (S y) = compare @{myord} x y
505505
506506\end{SaveVerbatim}
tutorial/examples/binary.idr+6−6
@@ -1,7 +1,7 @@
11module Main
22
33data Binary : Nat -> Type where
4− bEnd : Binary O
4+ bEnd : Binary Z
55 bO : Binary n -> Binary (n + n)
66 bI : Binary n -> Binary (S (n + n))
77
@@ -15,21 +15,21 @@ data Parity : Nat -> Type where
1515 odd : Parity (S (n + n))
1616
1717parity : (n:Nat) -> Parity n
18−parity O = even {n=O}
19−parity (S O) = odd {n=O}
18+parity Z = even {n=Z}
19+parity (S Z) = odd {n=Z}
2020parity (S (S k)) with (parity k)
2121 parity (S (S (j + j))) | even ?= even {n=S j}
2222 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
2323
2424natToBin : (n:Nat) -> Binary n
25−natToBin O = bEnd
25+natToBin Z = bEnd
2626natToBin (S k) with (parity k)
2727 natToBin (S (j + j)) | even = bI (natToBin j)
2828 natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))
2929
3030intToNat : Int -> Nat
31−intToNat 0 = O
32−intToNat x = if (x>0) then (S (intToNat (x-1))) else O
31+intToNat 0 = Z
32+intToNat x = if (x>0) then (S (intToNat (x-1))) else Z
3333
3434main : IO ()
3535main = do putStr "Enter a number: "
tutorial/examples/theorems.idr+14−14
@@ -5,15 +5,15 @@ fiveIsFive = refl
55twoPlusTwo : 2 + 2 = 4
66twoPlusTwo = refl
77
8−total disjoint : (n : Nat) -> O = S n -> _|_
8+total disjoint : (n : Nat) -> Z = S n -> _|_
99disjoint n p = replace {P = disjointTy} p ()
1010 where
1111 disjointTy : Nat -> Type
12− disjointTy O = ()
12+ disjointTy Z = ()
1313 disjointTy (S k) = _|_
1414
1515total acyclic : (n : Nat) -> n = S n -> _|_
16−acyclic O p = disjoint _ p
16+acyclic Z p = disjoint _ p
1717acyclic (S k) p = acyclic k (succInjective _ _ p)
1818
1919empty1 : _|_
@@ -24,33 +24,33 @@ empty1 = hd [] where
2424empty2 : _|_
2525empty2 = empty2
2626
27−plusReduces : (n:Nat) -> plus O n = n
27+plusReduces : (n:Nat) -> plus Z n = n
2828plusReduces n = refl
2929
30−plusReducesO : (n:Nat) -> n = plus n O
31−plusReducesO O = refl
32−plusReducesO (S k) = cong (plusReducesO k)
30+plusReducesZ : (n:Nat) -> n = plus n Z
31+plusReducesZ Z = refl
32+plusReducesZ (S k) = cong (plusReducesZ k)
3333
3434plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
35−plusReducesS O m = refl
35+plusReducesS Z m = refl
3636plusReducesS (S k) m = cong (plusReducesS k m)
3737
38−plusReducesO' : (n:Nat) -> n = plus n O
39−plusReducesO' O = ?plusredO_O
40−plusReducesO' (S k) = let ih = plusReducesO' k in
41− ?plusredO_S
38+plusReducesZ' : (n:Nat) -> n = plus n Z
39+plusReducesZ' Z = ?plusredZ_Z
40+plusReducesZ' (S k) = let ih = plusReducesZ' k in
41+ ?plusredZ_S
4242
4343
4444---------- Proofs ----------
4545
46−plusredO_S = proof {
46+plusredZ_S = proof {
4747 intro;
4848 intro;
4949 rewrite ih;
5050 trivial;
5151}
5252
53−plusredO_O = proof {
53+plusredZ_Z = proof {
5454 compute;
5555 trivial;
5656}
tutorial/examples/usefultypes.idr+1−1
@@ -10,7 +10,7 @@ vec = (_ ** [3, 4])
1010
1111list_lookup : Nat -> List a -> Maybe a
1212list_lookup _ Nil = Nothing
13−list_lookup O (x :: xs) = Just x
13+list_lookup Z (x :: xs) = Just x
1414list_lookup (S k) (x :: xs) = list_lookup k xs
1515
1616lookup_default : Nat -> List a -> a -> a
tutorial/examples/views.idr+3−3
@@ -5,14 +5,14 @@ data Parity : Nat -> Type where
55 odd : Parity (S (n + n))
66
77parity : (n:Nat) -> Parity n
8−parity O = even {n=O}
9−parity (S O) = odd {n=O}
8+parity Z = even {n=Z}
9+parity (S Z) = odd {n=Z}
1010parity (S (S k)) with (parity k)
1111 parity (S (S (j + j))) | even ?= even {n=S j}
1212 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
1313
1414natToBin : Nat -> List Bool
15−natToBin O = Nil
15+natToBin Z = Nil
1616natToBin k with (parity k)
1717 natToBin (j + j) | even = False :: natToBin j
1818 natToBin (S (j + j)) | odd = True :: natToBin j
tutorial/examples/wheres.idr+3−3
@@ -1,13 +1,13 @@
11module wheres
22
33even : Nat -> Bool
4−even O = True
4+even Z = True
55even (S k) = odd k where
6− odd O = False
6+ odd Z = False
77 odd (S k) = even k
88
99test : List Nat
10−test = [c (S 1), c O, d (S O)]
10+test = [c (S 1), c Z, d (S Z)]
1111 where c x = 42 + x
1212 d y = c (y + 1 + z y)
1313 where z w = y + w
tutorial/provisional.tex+6−6
@@ -22,8 +22,8 @@ We'd like to implement this as follows:
2222\begin{SaveVerbatim}{parfail}
2323
2424parity : (n:Nat) -> Parity n
25−parity O = even {n=O}
26−parity (S O) = odd {n=O}
25+parity Z = even {n=Z}
26+parity (S Z) = odd {n=Z}
2727parity (S (S k)) with (parity k)
2828 parity (S (S (j + j))) | even = even {n=S j}
2929 parity (S (S (S (j + j)))) | odd = odd {n=S j}
@@ -77,8 +77,8 @@ except that they introduce the right hand side with a \texttt{?=} rathar than
7777\begin{SaveVerbatim}{paritypro}
7878
7979parity : (n:Nat) -> Parity n
80−parity O = even {n=O}
81−parity (S O) = odd {n=O}
80+parity Z = even {n=Z}
81+parity (S Z) = odd {n=Z}
8282parity (S (S k)) with (parity k)
8383 parity (S (S (j + j))) | even ?= even {n=S j}
8484 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
@@ -231,7 +231,7 @@ case \texttt{Nat}):
231231\begin{SaveVerbatim}{bindef}
232232
233233data Binary : Nat -> Type where
234− bEnd : Binary O
234+ bEnd : Binary Z
235235 bO : Binary n -> Binary (n + n)
236236 bI : Binary n -> Binary (S (n + n))
237237
@@ -263,7 +263,7 @@ provisional definition in the odd case:
263263\begin{SaveVerbatim}{ntbdef}
264264
265265natToBin : (n:Nat) -> Binary n
266−natToBin O = bEnd
266+natToBin Z = bEnd
267267natToBin (S k) with (parity k)
268268 natToBin (S (j + j)) | even = bI (natToBin j)
269269 natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))
tutorial/theorems.tex+46−46
@@ -42,11 +42,11 @@ to a successor:
4242
4343\begin{SaveVerbatim}{natdisjoint}
4444
45−disjoint : (n : Nat) -> O = S n -> _|_
45+disjoint : (n : Nat) -> Z = S n -> _|_
4646disjoint n p = replace {P = disjointTy} p ()
4747 where
4848 disjointTy : Nat -> Type
49− disjointTy O = ()
49+ disjointTy Z = ()
5050 disjointTy (S k) = _|_
5151
5252\end{SaveVerbatim}
@@ -76,7 +76,7 @@ we want to prove the following theorem about the reduction behaviour of \texttt{
7676
7777\begin{SaveVerbatim}{plusred}
7878
79−plusReduces : (n:Nat) -> plus O n = n
79+plusReduces : (n:Nat) -> plus Z n = n
8080
8181\end{SaveVerbatim}
8282\useverb{plusred}
@@ -90,7 +90,7 @@ of interest.
9090
9191We won't go into details here, but the Curry-Howard
9292correspondence~\cite{howard} explains this relationship.
93−The proof itself is trivial, because \texttt{plus O n} normalises to \texttt{n}
93+The proof itself is trivial, because \texttt{plus Z n} normalises to \texttt{n}
9494by the definition of \texttt{plus}:
9595
9696\begin{SaveVerbatim}{plusredp}
@@ -107,9 +107,9 @@ on the first argument to \texttt{plus}, namely \texttt{n}.
107107
108108\begin{SaveVerbatim}{plusRedO}
109109
110−plusReducesO : (n:Nat) -> n = plus n O
111−plusReducesO O = refl
112−plusReducesO (S k) = cong (plusReducesO k)
110+plusReducesZ : (n:Nat) -> n = plus n Z
111+plusReducesZ Z = refl
112+plusReducesZ (S k) = cong (plusReducesZ k)
113113
114114\end{SaveVerbatim}
115115\useverb{plusRedO}
@@ -131,7 +131,7 @@ We can do the same for the reduction behaviour of plus on successors:
131131\begin{SaveVerbatim}{plusRedS}
132132
133133plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
134−plusReducesS O m = refl
134+plusReducesS Z m = refl
135135plusReducesS (S k) m = cong (plusReducesS k m)
136136
137137\end{SaveVerbatim}
@@ -148,16 +148,16 @@ therefore provides an interactive proof mode.
148148Instead of writing the proof in one go, we can use \Idris{}'s interactive
149149proof mode. To do this, we write the general \emph{structure} of the proof,
150150and use the interactive mode to complete the details. We'll be constructing
151−the proof by \emph{induction}, so we write the cases for \texttt{O} and
151+the proof by \emph{induction}, so we write the cases for \texttt{Z} and
152152\texttt{S}, with a recursive call in the \texttt{S} case giving the inductive
153153hypothesis, and insert \emph{metavariables} for the rest of the definition:
154154
155155\begin{SaveVerbatim}{prOstruct}
156156
157−plusReducesO' : (n:Nat) -> n = plus n O
158−plusReducesO' O = ?plusredO_O
159−plusReducesO' (S k) = let ih = plusReducesO' k in
160− ?plusredO_S
157+plusReducesZ' : (n:Nat) -> n = plus n Z
158+plusReducesZ' Z = ?plusredZ_Z
159+plusReducesZ' (S k) = let ih = plusReducesZ' k in
160+ ?plusredZ_S
161161
162162\end{SaveVerbatim}
163163\useverb{prOstruct}
@@ -173,17 +173,17 @@ precisely, which functions exist but have no definitions), then the
173173
174174*theorems> :m
175175Global metavariables:
176− [plusredO_S,plusredO_O]
176+ [plusredZ_S,plusredZ_Z]
177177
178178\end{SaveVerbatim}
179179
180180\begin{SaveVerbatim}{metatypes}
181181
182−*theorems> :t plusredO_O
183−plusredO_O : O = plus O O
182+*theorems> :t plusredZ_Z
183+plusredZ_Z : Z = plus Z Z
184184
185−*theorems> :t plusredO_S
186−plusredO_S : (k : Nat) -> (k = plus k O) -> S k = S (plus k O)
185+*theorems> :t plusredZ_S
186+plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = S (plus k Z)
187187
188188\end{SaveVerbatim}
189189\useverb{showmetas}
@@ -196,10 +196,10 @@ the missing definitions.
196196
197197\begin{SaveVerbatim}{proveO}
198198
199−*theorems> :p plusredO_O
199+*theorems> :p plusredZ_Z
200200
201−---------------------------------- (plusredO_O) --------
202−{hole0} : O = plus O O
201+---------------------------------- (plusredZ_Z) --------
202+{hole0} : Z = plus Z Z
203203
204204\end{SaveVerbatim}
205205\useverb{proveO}
@@ -213,24 +213,24 @@ we can normalise the goal with the \texttt{compute} tactic:
213213
214214\begin{SaveVerbatim}{compute}
215215
216−-plusredO_O> compute
216+-plusredZ_Z> compute
217217
218−---------------------------------- (plusredO_O) --------
219−{hole0} : O = O
218+---------------------------------- (plusredZ_Z) --------
219+{hole0} : Z = Z
220220
221221\end{SaveVerbatim}
222222\useverb{compute}
223223
224224\noindent
225−Now we have to prove that \texttt{O} equals \texttt{O}, which is easy to prove by
225+Now we have to prove that \texttt{Z} equals \texttt{Z}, which is easy to prove by
226226\texttt{refl}. To apply a function, such as \texttt{refl}, we use \texttt{refine}
227227which introduces subgoals for each of the function's explicit arguments (\texttt{refl}
228228has none):
229229
230230\begin{SaveVerbatim}{refrefl}
231231
232−-plusredO_O> refine refl
233−plusredO_O: no more goals
232+-plusredZ_Z> refine refl
233+plusredZ_Z: no more goals
234234
235235\end{SaveVerbatim}
236236\useverb{refrefl}
@@ -244,8 +244,8 @@ This also outputs a trace of the proof:
244244
245245\begin{SaveVerbatim}{prOprooftrace}
246246
247−-plusredO_O> qed
248−plusredO_O = proof {
247+-plusredZ_Z> qed
248+plusredZ_Z = proof {
249249 compute;
250250 refine refl;
251251}
@@ -257,7 +257,7 @@ plusredO_O = proof {
257257
258258*theorems> :m
259259Global metavariables:
260− [plusredO_S]
260+ [plusredZ_S]
261261
262262\end{SaveVerbatim}
263263\useverb{showmetasO}
@@ -269,10 +269,10 @@ Let us now prove the other required lemma, \texttt{plusredO\_S}:
269269
270270\begin{SaveVerbatim}{plusredOSprf}
271271
272−*theorems> :p plusredO_S
272+*theorems> :p plusredZ_S
273273
274−---------------------------------- (plusredO_S) --------
275−{hole0} : (k : Nat) -> (k = plus k O) -> S k = S (plus k O)
274+---------------------------------- (plusredZ_S) --------
275+{hole0} : (k : Nat) -> (k = plus k Z) -> S k = S (plus k Z)
276276
277277\end{SaveVerbatim}
278278\useverb{plusredOSprf}
@@ -286,28 +286,28 @@ twice (or \texttt{intros}, which introduces all arguments as premisses). This gi
286286\begin{SaveVerbatim}{prSintros}
287287
288288 k : Nat
289− ih : k = plus k O
290−---------------------------------- (plusredO_S) --------
291−{hole2} : S k = S (plus k O)
289+ ih : k = plus k Z
290+---------------------------------- (plusredZ_S) --------
291+{hole2} : S k = S (plus k Z)
292292
293293\end{SaveVerbatim}
294294\useverb{prSintros}
295295
296296\noindent
297−We know, from the type of \texttt{ih}, that \texttt{k = plus k O}, so we would like to
298−use this knowledge to replace \texttt{plus k O} in the goal with \texttt{k}. We can
297+We know, from the type of \texttt{ih}, that \texttt{k = plus k Z}, so we would like to
298+use this knowledge to replace \texttt{plus k Z} in the goal with \texttt{k}. We can
299299achieve this with the \texttt{rewrite} tactic:
300300
301301\begin{SaveVerbatim}{}
302302
303−-plusredO_S> rewrite ih
303+-plusredZ_S> rewrite ih
304304
305305 k : Nat
306− ih : k = plus k O
307−---------------------------------- (plusredO_S) --------
306+ ih : k = plus k Z
307+---------------------------------- (plusredZ_S) --------
308308{hole3} : S k = S k
309309
310−-plusredO_S>
310+-plusredZ_S>
311311
312312\end{SaveVerbatim}
313313\useverb{}
@@ -318,10 +318,10 @@ the goal using that proof. Here, it results in an equality which is trivially pr
318318
319319\begin{SaveVerbatim}{prOStrace}
320320
321−-plusredO_S> trivial
322−plusredO_S: no more goals
323−-plusredO_S> qed
324−plusredO_S = proof {
321+-plusredZ_S> trivial
322+plusredZ_S: no more goals
323+-plusredZ_S> qed
324+plusredZ_S = proof {
325325 intros;
326326 rewrite ih;
327327 trivial;
tutorial/typesfuns.tex+24−24
@@ -81,7 +81,7 @@ syntax. Natural numbers and lists, for example, can be declared as follows:
8181
8282\begin{SaveVerbatim}{natlist}
8383
84−data Nat = O | S Nat -- Natural numbers
84+data Nat = Z | S Nat -- Natural numbers
8585 -- (zero and successor)
8686data List a = Nil | (::) a (List a) -- Polymorphic lists
8787
@@ -90,7 +90,7 @@ data List a = Nil | (::) a (List a) -- Polymorphic lists
9090
9191\noindent
9292The above declarations are taken from the standard library. Unary natural
93−numbers can be either zero (\texttt{O} - that's a capital letter 'o', not the digit), or
93+numbers can be either zero (\texttt{Z}), or
9494the successor of another natural number (\texttt{S k}).
9595Lists can either be empty (\texttt{Nil})
9696or a value added to the front of another list (\texttt{x :: xs}).
@@ -132,12 +132,12 @@ defined as follows, again taken from the standard library:
132132
133133-- Unary addition
134134plus : Nat -> Nat -> Nat
135−plus O y = y
135+plus Z y = y
136136plus (S k) y = S (plus k y)
137137
138138-- Unary multiplication
139139mult : Nat -> Nat -> Nat
140−mult O y = O
140+mult Z y = Z
141141mult (S k) y = plus y (mult k y)
142142
143143\end{SaveVerbatim}
@@ -148,7 +148,7 @@ The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded
148148for use by \texttt{Nat}, and are implemented
149149using the above functions. Unlike Haskell, there is no restriction on whether
150150types and function names must begin with a capital letter or not. Function
151−names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S},
151+names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{Z}, \tDC{S},
152152\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are
153153all part of the same namespace.
154154
@@ -156,10 +156,10 @@ We can test these functions at the \Idris{} prompt:
156156
157157\begin{SaveVerbatim}{fntest}
158158
159−Idris> plus (S (S O)) (S (S O))
160−S (S (S (S O))) : Nat
161−Idris> mult (S (S (S O))) (plus (S (S O)) (S (S O)))
162−S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat
159+Idris> plus (S (S Z)) (S (S Z))
160+S (S (S (S Z))) : Nat
161+Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
162+S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) : Nat
163163
164164\end{SaveVerbatim}
165165\useverb{fntest}
@@ -171,9 +171,9 @@ meaning that we can also test the functions as follows:
171171\begin{SaveVerbatim}{fntest}
172172
173173Idris> plus 2 2
174−S (S (S (S O))) : Nat
174+S (S (S (S Z))) : Nat
175175Idris> mult 3 (plus 2 2)
176−S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat
176+S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) : Nat
177177
178178\end{SaveVerbatim}
179179\useverb{fntest}
@@ -252,13 +252,13 @@ So, for example, the following definitions are legal:
252252\begin{SaveVerbatim}{whereinfer}
253253
254254even : Nat -> Bool
255−even O = True
255+even Z = True
256256even (S k) = odd k where
257− odd O = False
257+ odd Z = False
258258 odd (S k) = even k
259259
260260test : List Nat
261−test = [c (S 1), c O, d (S O)]
261+test = [c (S 1), c Z, d (S Z)]
262262 where c x = 42 + x
263263 d y = c (y + 1 + z y)
264264 where z w = y + w
@@ -278,7 +278,7 @@ we declare vectors as follows:
278278\begin{SaveVerbatim}{vect}
279279
280280data Vect : Type -> Nat -> Type where
281− Nil : Vect a O
281+ Nil : Vect a Z
282282 (::) : a -> Vect a k -> Vect a (S k)
283283
284284\end{SaveVerbatim}
@@ -366,12 +366,12 @@ data Fin : Nat -> Type where
366366\useverb{findecl}
367367
368368\noindent
369−\tDC{fO} is the zeroth element of a finite set with \texttt{S k} elements;
369+\tDC{fO} is the zeroth element of a finite set with \texttt{S k} elements;
370370\texttt{fS n} is the
371371\texttt{n+1}th element of a finite set with \texttt{S k} elements.
372372\tTC{Fin} is indexed by a \tTC{Nat}, which
373373represents the number of elements in the set. Obviously we can't construct an
374−element of an empty set, so neither constructor targets \texttt{Fin O}.
374+element of an empty set, so neither constructor targets \texttt{Fin Z}.
375375
376376A useful application of the \tTC{Fin} family is to represent bounded
377377natural numbers. Since the first \tTC{n} natural numbers form a finite
@@ -397,10 +397,10 @@ need for a run-time bounds check. The type checker guarantees that the location
397397is no larger than the length of the vector.
398398
399399Note also that there is no case for \texttt{Nil} here. This is because it is
400−impossible. Since there is no element of \texttt{Fin O}, and the location is a
401−\texttt{Fin n}, then \texttt{n} can not be \tDC{O}. As a result, attempting to
400+impossible. Since there is no element of \texttt{Fin Z}, and the location is a
401+\texttt{Fin n}, then \texttt{n} can not be \tDC{Z}. As a result, attempting to
402402look up an element in an empty vector would give a compile time type error,
403−since it would force \texttt{n} to be \tDC{O}.
403+since it would force \texttt{n} to be \tDC{Z}.
404404
405405\subsubsection{Implicit Arguments}
406406
@@ -520,11 +520,11 @@ data types and functions to be defined simultaneously:
520520
521521mutual
522522 even : Nat -> Bool
523− even O = True
523+ even Z = True
524524 even (S k) = odd k
525525
526526 odd : Nat -> Bool
527− odd O = False
527+ odd Z = False
528528 odd (S k) = even k
529529
530530\end{SaveVerbatim}
@@ -663,7 +663,7 @@ We have already seen the \texttt{List} and \texttt{Vect} data types:
663663data List a = Nil | (::) a (List a)
664664
665665data Vect : Type -> Nat -> Type where
666− Nil : Vect a O
666+ Nil : Vect a Z
667667 (::) : a -> Vect a k -> Vect a (S k)
668668
669669\end{SaveVerbatim}
@@ -787,7 +787,7 @@ bounds error:
787787
788788list_lookup : Nat -> List a -> Maybe a
789789list_lookup _ Nil = Nothing
790−list_lookup O (x :: xs) = Just x
790+list_lookup Z (x :: xs) = Just x
791791list_lookup (S k) (x :: xs) = list_lookup k xs
792792
793793\end{SaveVerbatim}
tutorial/views.tex+2−2
@@ -10,7 +10,7 @@ determined by whether the vector was empty or not:
1010\begin{SaveVerbatim}{appdep}
1111
1212(++) : Vect a n -> Vect a m -> Vect a (n + m)
13−(++) {n=O} [] ys = ys
13+(++) {n=Z} [] ys = ys
1414(++) {n=S k} (x :: xs) ys = x :: xs ++ ys
1515
1616\end{SaveVerbatim}
@@ -83,7 +83,7 @@ to write a function which converts a natural number to a list of binary digits
8383\begin{SaveVerbatim}{natToBin}
8484
8585natToBin : Nat -> List Bool
86−natToBin O = Nil
86+natToBin Z = Nil
8787natToBin k with (parity k)
8888 natToBin (j + j) | even = False :: natToBin j
8989 natToBin (S (j + j)) | odd = True :: natToBin j