2311d55 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

rename O into Z

2311d55raichoo13 years ago

effects/Effect/Memory.idr+1−1

compare with master

unifiedsplit

@@ -63,7 +63,7 @@ do_memmove dest src dest_offset src_offset size

64private

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

67do_peek ptr offset (S n)

68 = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FByte) ptr (fromInteger $ cast offset)

69 bs <- do_peek ptr (S offset) n

effects/Effects.idr+2−2

@@ -63,13 +63,13 @@ rebuildEnv (x :: xs) SubNil [] = x :: xs

64-- some proof automation

65findEffElem : 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

67findEffElem (S n) ctxt goal = GoalType "EffElem"

68 (Try (Refine "Here" `Seq` Solve)

69 (Refine "There" `Seq` (Solve `Seq` findEffElem n ctxt goal)))

71findSubList : 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

73findSubList (S n) ctxt goal

74 = GoalType "SubList"

75 (Try (Refine "subListId" `Seq` Solve)

lib/Data/Bits.idr+102−102

@@ -4,11 +4,11 @@ module Data.Bits

5divCeil : Nat -> Nat -> Nat

6divCeil x y = case x `mod` y of

7− O => x `div` y

7+ Z => x `div` y

8 S _ => S (x `div` y)

10nextPow2 : Nat -> Nat

11−nextPow2 O = O

11+nextPow2 Z = Z

12nextPow2 x = if x == (2 `power` l2x)

13 then l2x

14 else S l2x

@@ -19,9 +19,9 @@ nextBytes : Nat -> Nat

19nextBytes bits = (nextPow2 (bits `divCeil` 8))

21machineTy : Nat -> Type

22−machineTy O = Bits8

22+machineTy Z = Bits8

23−machineTy (S O) = Bits16

23+machineTy (S Z) = Bits16

24−machineTy (S (S O)) = Bits32

24+machineTy (S (S Z)) = Bits32

25machineTy (S (S (S _))) = Bits64

27bitsUsed : Nat -> Nat

@@ -29,19 +29,19 @@ bitsUsed n = 8 * (2 `power` n)

30%assert_total

31natToBits' : machineTy n -> Nat -> machineTy n

32−natToBits' a O = a

32+natToBits' a Z = a

33natToBits' {n=n} a x with n

34 -- 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'

35+ natToBits' a (S x') | Z = 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'

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 O) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x'

37+ natToBits' a (S x') | S (S Z) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x'

38 natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'

40natToBits : Nat -> machineTy n

41natToBits {n=n} x with n

42− | O = natToBits' {n=0} (prim__truncInt_B8 0) x

42+ | Z = natToBits' {n=0} (prim__truncInt_B8 0) x

43− | S O = natToBits' {n=1} (prim__truncInt_B16 0) x

43+ | S Z = natToBits' {n=1} (prim__truncInt_B16 0) x

44− | S (S O) = natToBits' {n=2} (prim__truncInt_B32 0) x

44+ | S (S Z) = natToBits' {n=2} (prim__truncInt_B32 0) x

45 | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x

47getPad : Nat -> machineTy n

@@ -94,9 +94,9 @@ pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad

95shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

96shiftLeft' {n=n} x c with (nextBytes n)

97− | O = pad8' n prim__shlB8 x c

97+ | Z = pad8' n prim__shlB8 x c

98− | S O = pad16' n prim__shlB16 x c

98+ | S Z = pad16' n prim__shlB16 x c

99− | S (S O) = pad32' n prim__shlB32 x c

99+ | S (S Z) = pad32' n prim__shlB32 x c

100 | S (S (S _)) = pad64' n prim__shlB64 x c

101

102public

@@ -105,9 +105,9 @@ shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)

105

106shiftRightLogical' : machineTy n -> machineTy n -> machineTy n

107shiftRightLogical' {n=n} x c with n

108− | O = prim__lshrB8 x c

108+ | Z = prim__lshrB8 x c

109− | S O = prim__lshrB16 x c

109+ | S Z = prim__lshrB16 x c

110− | S (S O) = prim__lshrB32 x c

110+ | S (S Z) = prim__lshrB32 x c

111 | S (S (S _)) = prim__lshrB64 x c

112

113public

@@ -117,9 +117,9 @@ shiftRightLogical {n} (MkBits x) (MkBits y)

117

118shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

119shiftRightArithmetic' {n=n} x c with (nextBytes n)

120− | O = pad8' n prim__ashrB8 x c

120+ | Z = pad8' n prim__ashrB8 x c

121− | S O = pad16' n prim__ashrB16 x c

121+ | S Z = pad16' n prim__ashrB16 x c

122− | S (S O) = pad32' n prim__ashrB32 x c

122+ | S (S Z) = pad32' n prim__ashrB32 x c

123 | S (S (S _)) = pad64' n prim__ashrB64 x c

124

125public

@@ -128,9 +128,9 @@ shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)

128

129and' : machineTy n -> machineTy n -> machineTy n

130and' {n=n} x y with n

131− | O = prim__andB8 x y

131+ | Z = prim__andB8 x y

132− | S O = prim__andB16 x y

132+ | S Z = prim__andB16 x y

133− | S (S O) = prim__andB32 x y

133+ | S (S Z) = prim__andB32 x y

134 | S (S (S _)) = prim__andB64 x y

135

136public

@@ -139,9 +139,9 @@ and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)

139

140or' : machineTy n -> machineTy n -> machineTy n

141or' {n=n} x y with n

142− | O = prim__orB8 x y

142+ | Z = prim__orB8 x y

143− | S O = prim__orB16 x y

143+ | S Z = prim__orB16 x y

144− | S (S O) = prim__orB32 x y

144+ | S (S Z) = prim__orB32 x y

145 | S (S (S _)) = prim__orB64 x y

146

147public

@@ -150,9 +150,9 @@ or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)

150

151xor' : machineTy n -> machineTy n -> machineTy n

152xor' {n=n} x y with n

153− | O = prim__xorB8 x y

153+ | Z = prim__xorB8 x y

154− | S O = prim__xorB16 x y

154+ | S Z = prim__xorB16 x y

155− | S (S O) = prim__xorB32 x y

155+ | S (S Z) = prim__xorB32 x y

156 | S (S (S _)) = prim__xorB64 x y

157

158public

@@ -161,9 +161,9 @@ xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)

161

162plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

163plus' {n=n} x y with (nextBytes n)

164− | O = pad8 n prim__addB8 x y

164+ | Z = pad8 n prim__addB8 x y

165− | S O = pad16 n prim__addB16 x y

165+ | S Z = pad16 n prim__addB16 x y

166− | S (S O) = pad32 n prim__addB32 x y

166+ | S (S Z) = pad32 n prim__addB32 x y

167 | S (S (S _)) = pad64 n prim__addB64 x y

168

169public

@@ -172,9 +172,9 @@ plus (MkBits x) (MkBits y) = MkBits (plus' x y)

172

173minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

174minus' {n=n} x y with (nextBytes n)

175− | O = pad8 n prim__subB8 x y

175+ | Z = pad8 n prim__subB8 x y

176− | S O = pad16 n prim__subB16 x y

176+ | S Z = pad16 n prim__subB16 x y

177− | S (S O) = pad32 n prim__subB32 x y

177+ | S (S Z) = pad32 n prim__subB32 x y

178 | S (S (S _)) = pad64 n prim__subB64 x y

179

180public

@@ -183,9 +183,9 @@ minus (MkBits x) (MkBits y) = MkBits (minus' x y)

183

184times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

185times' {n=n} x y with (nextBytes n)

186− | O = pad8 n prim__mulB8 x y

186+ | Z = pad8 n prim__mulB8 x y

187− | S O = pad16 n prim__mulB16 x y

187+ | S Z = pad16 n prim__mulB16 x y

188− | S (S O) = pad32 n prim__mulB32 x y

188+ | S (S Z) = pad32 n prim__mulB32 x y

189 | S (S (S _)) = pad64 n prim__mulB64 x y

190

191public

@@ -195,9 +195,9 @@ times (MkBits x) (MkBits y) = MkBits (times' x y)

195partial

196sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

197sdiv' {n=n} x y with (nextBytes n)

198− | O = prim__sdivB8 x y

198+ | Z = prim__sdivB8 x y

199− | S O = prim__sdivB16 x y

199+ | S Z = prim__sdivB16 x y

200− | S (S O) = prim__sdivB32 x y

200+ | S (S Z) = prim__sdivB32 x y

201 | S (S (S _)) = prim__sdivB64 x y

202

203public partial

@@ -207,9 +207,9 @@ sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)

207partial

208udiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

209udiv' {n=n} x y with (nextBytes n)

210− | O = prim__udivB8 x y

210+ | Z = prim__udivB8 x y

211− | S O = prim__udivB16 x y

211+ | S Z = prim__udivB16 x y

212− | S (S O) = prim__udivB32 x y

212+ | S (S Z) = prim__udivB32 x y

213 | S (S (S _)) = prim__udivB64 x y

214

215public partial

@@ -219,9 +219,9 @@ udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)

219partial

220srem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

221srem' {n=n} x y with (nextBytes n)

222− | O = prim__sremB8 x y

222+ | Z = prim__sremB8 x y

223− | S O = prim__sremB16 x y

223+ | S Z = prim__sremB16 x y

224− | S (S O) = prim__sremB32 x y

224+ | S (S Z) = prim__sremB32 x y

225 | S (S (S _)) = prim__sremB64 x y

226

227public partial

@@ -231,9 +231,9 @@ srem (MkBits x) (MkBits y) = MkBits (srem' x y)

231partial

232urem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

233urem' {n=n} x y with (nextBytes n)

234− | O = prim__uremB8 x y

234+ | Z = prim__uremB8 x y

235− | S O = prim__uremB16 x y

235+ | S Z = prim__uremB16 x y

236− | S (S O) = prim__uremB32 x y

236+ | S (S Z) = prim__uremB32 x y

237 | S (S (S _)) = prim__uremB64 x y

238

239public partial

@@ -243,37 +243,37 @@ urem (MkBits x) (MkBits y) = MkBits (urem' x y)

243-- TODO: Proofy comparisons via postulates

244lt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

245lt {n=n} x y with (nextBytes n)

246− | O = prim__ltB8 x y

246+ | Z = prim__ltB8 x y

247− | S O = prim__ltB16 x y

247+ | S Z = prim__ltB16 x y

248− | S (S O) = prim__ltB32 x y

248+ | S (S Z) = prim__ltB32 x y

249 | S (S (S _)) = prim__ltB64 x y

250

251lte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

252lte {n=n} x y with (nextBytes n)

253− | O = prim__lteB8 x y

253+ | Z = prim__lteB8 x y

254− | S O = prim__lteB16 x y

254+ | S Z = prim__lteB16 x y

255− | S (S O) = prim__lteB32 x y

255+ | S (S Z) = prim__lteB32 x y

256 | S (S (S _)) = prim__lteB64 x y

257

258eq : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

259eq {n=n} x y with (nextBytes n)

260− | O = prim__eqB8 x y

260+ | Z = prim__eqB8 x y

261− | S O = prim__eqB16 x y

261+ | S Z = prim__eqB16 x y

262− | S (S O) = prim__eqB32 x y

262+ | S (S Z) = prim__eqB32 x y

263 | S (S (S _)) = prim__eqB64 x y

264

265gte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

266gte {n=n} x y with (nextBytes n)

267− | O = prim__gteB8 x y

267+ | Z = prim__gteB8 x y

268− | S O = prim__gteB16 x y

268+ | S Z = prim__gteB16 x y

269− | S (S O) = prim__gteB32 x y

269+ | S (S Z) = prim__gteB32 x y

270 | S (S (S _)) = prim__gteB64 x y

271

272gt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

273gt {n=n} x y with (nextBytes n)

274− | O = prim__gtB8 x y

274+ | Z = prim__gtB8 x y

275− | S O = prim__gtB16 x y

275+ | S Z = prim__gtB16 x y

276− | S (S O) = prim__gtB32 x y

276+ | S (S Z) = prim__gtB32 x y

277 | S (S (S _)) = prim__gtB64 x y

278

279instance Eq (Bits n) where

@@ -293,11 +293,11 @@ instance Ord (Bits n) where

293

294complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)

295complement' {n=n} x with (nextBytes n)

296− | O = let pad = getPad {n=0} n in

296+ | Z = let pad = getPad {n=0} n in

297 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

299 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

301 prim__complB32 (x `prim__shlB32` pad) `prim__lshrB32` pad

302 | S (S (S _)) = let pad = getPad {n=3} n in

303 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad

@@ -309,15 +309,15 @@ complement (MkBits x) = MkBits (complement' x)

309-- TODO: Prove

310zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

311zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

312− | (O, O) = believe_me x

312+ | (Z, Z) = believe_me x

313− | (O, S O) = believe_me (prim__zextB8_B16 (believe_me x))

313+ | (Z, S Z) = believe_me (prim__zextB8_B16 (believe_me x))

314− | (O, S (S O)) = believe_me (prim__zextB8_B32 (believe_me x))

314+ | (Z, S (S Z)) = believe_me (prim__zextB8_B32 (believe_me x))

315− | (O, S (S (S _))) = believe_me (prim__zextB8_B64 (believe_me x))

315+ | (Z, S (S (S _))) = believe_me (prim__zextB8_B64 (believe_me x))

316− | (S O, S O) = believe_me x

316+ | (S Z, S Z) = believe_me x

317− | (S O, S (S O)) = believe_me (prim__zextB16_B32 (believe_me x))

317+ | (S Z, S (S Z)) = believe_me (prim__zextB16_B32 (believe_me x))

318− | (S O, S (S (S _))) = believe_me (prim__zextB16_B64 (believe_me x))

318+ | (S Z, S (S (S _))) = believe_me (prim__zextB16_B64 (believe_me x))

319− | (S (S O), S (S O)) = believe_me x

319+ | (S (S Z), S (S Z)) = believe_me x

320− | (S (S O), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))

320+ | (S (S Z), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))

321 | (S (S (S _)), S (S (S _))) = believe_me x

322

323public

@@ -327,11 +327,11 @@ zeroExtend (MkBits x) = MkBits (zext' x)

327%assert_total

328intToBits' : Integer -> machineTy (nextBytes n)

329intToBits' {n=n} x with (nextBytes n)

330− | O = let pad = getPad {n=0} n in

330+ | Z = let pad = getPad {n=0} n in

331 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

333 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

335 prim__lshrB32 (prim__shlB32 (prim__truncBigInt_B32 x) pad) pad

336 | S (S (S _)) = let pad = getPad {n=3} n in

337 prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad

@@ -345,9 +345,9 @@ instance Cast Integer (Bits n) where

345

346bitsToInt' : machineTy (nextBytes n) -> Integer

347bitsToInt' {n=n} x with (nextBytes n)

348− | O = prim__zextB8_BigInt x

348+ | Z = prim__zextB8_BigInt x

349− | S O = prim__zextB16_BigInt x

349+ | S Z = prim__zextB16_BigInt x

350− | S (S O) = prim__zextB32_BigInt x

350+ | S (S Z) = prim__zextB32_BigInt x

351 | S (S (S _)) = prim__zextB64_BigInt x

352

353public

@@ -364,28 +364,28 @@ bitsToInt (MkBits x) = bitsToInt' x

364-- TODO: Prove

365sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

366sext' {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

368 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

370 believe_me (prim__ashrB16 (prim__sextB8_B16 (prim__shlB8 (believe_me x) pad))

371 (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

373 believe_me (prim__ashrB32 (prim__sextB8_B32 (prim__shlB8 (believe_me x) pad))

374 (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

376 believe_me (prim__ashrB64 (prim__sextB8_B64 (prim__shlB8 (believe_me x) pad))

377 (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

379 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

381 believe_me (prim__ashrB32 (prim__sextB16_B32 (prim__shlB16 (believe_me x) pad))

382 (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

384 believe_me (prim__ashrB64 (prim__sextB16_B64 (prim__shlB16 (believe_me x) pad))

385 (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

387 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

389 believe_me (prim__ashrB64 (prim__sextB32_B64 (prim__shlB32 (believe_me x) pad))

390 (prim__zextB32_B64 pad))

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

398-- TODO: Prove

399trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)

400trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

401− | (O, O) = believe_me x

401+ | (Z, Z) = believe_me x

402− | (O, S O) = believe_me (prim__truncB16_B8 (believe_me x))

402+ | (Z, S Z) = believe_me (prim__truncB16_B8 (believe_me x))

403− | (O, S (S O)) = believe_me (prim__truncB32_B8 (believe_me x))

403+ | (Z, S (S Z)) = believe_me (prim__truncB32_B8 (believe_me x))

404− | (O, S (S (S _))) = believe_me (prim__truncB64_B8 (believe_me x))

404+ | (Z, S (S (S _))) = believe_me (prim__truncB64_B8 (believe_me x))

405− | (S O, S O) = believe_me x

405+ | (S Z, S Z) = believe_me x

406− | (S O, S (S O)) = believe_me (prim__truncB32_B16 (believe_me x))

406+ | (S Z, S (S Z)) = believe_me (prim__truncB32_B16 (believe_me x))

407− | (S O, S (S (S _))) = believe_me (prim__truncB64_B16 (believe_me x))

407+ | (S Z, S (S (S _))) = believe_me (prim__truncB64_B16 (believe_me x))

408− | (S (S O), S (S O)) = believe_me x

408+ | (S (S Z), S (S Z)) = believe_me x

409− | (S (S O), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))

409+ | (S (S Z), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))

410 | (S (S (S _)), S (S (S _))) = believe_me x

411

412--public

lib/Data/BoundedList.idr+3−3

@@ -34,7 +34,7 @@ weaken (x :: xs) = x :: weaken xs

35take : (n : Nat) -> List a -> BoundedList a n

36take _ [] = []

37−take O _ = []

37+take Z _ = []

38take (S n') (x :: xs) = x :: take n' xs

40toList : BoundedList a n -> List a

@@ -50,7 +50,7 @@ fromList (x :: xs) = x :: fromList xs

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

52replicate : (n : Nat) -> a -> BoundedList a n

53−replicate O _ = []

53+replicate Z _ = []

54replicate (S n) x = x :: replicate n x

56--------------------------------------------------------------------------------

@@ -79,7 +79,7 @@ map f (x :: xs) = f x :: map f xs

80%assert_total -- not sure why this isn't accepted - clearly decreasing on n

81pad : (xs : BoundedList a n) -> (padding : a) -> BoundedList a n

82−pad {n=O} [] _ = []

82+pad {n=Z} [] _ = []

83pad {n=S n'} [] padding = padding :: (pad {n=n'} [] padding)

84pad {n=S n'} (x :: xs) padding = x :: pad {n=n'} xs padding

lib/Data/HVect.idr+1−1

@@ -40,7 +40,7 @@ using (k : Nat, ts : Vect Type k)

40 class Shows (k : Nat) (ts : Vect Type k) where

41 shows : HVect ts -> Vect String k

43− instance Shows O [] where

43+ instance Shows Z [] where

44 shows [] = []

46 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

3-- TODO: write merge and split

5data Tree : Nat -> Type -> Type -> Type where

6− Leaf : k -> v -> Tree O k v

6+ Leaf : k -> v -> Tree Z k v

7 Branch2 : Tree n k v -> k -> Tree n k v -> Tree (S n) k v

8 Branch3 : Tree n k v -> k -> Tree n k v -> k -> Tree n k v -> Tree (S n) k v

@@ -123,7 +123,7 @@ treeInsert k v t =

123 Right (a, b, c) => Right (Branch2 a b c)

124

125delType : Nat -> Type -> Type -> Type

126−delType O k v = ()

126+delType Z k v = ()

127delType (S n) k v = Tree n k v

128

129treeDelete : 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) =

132 Right ()

133 else

134 Left (Leaf k' v)

135−treeDelete {n=S O} k (Branch2 t1 k' t2) =

135+treeDelete {n=S Z} k (Branch2 t1 k' t2) =

136 if k <= k' then

137 case treeDelete k t1 of

138 Left t1' => Left (Branch2 t1' k' t2)

@@ -141,7 +141,7 @@ treeDelete {n=S O} k (Branch2 t1 k' t2) =

141 case treeDelete k t2 of

142 Left t2' => Left (Branch2 t1 k' t2')

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

145 if k <= k1 then

146 case treeDelete k t1 of

147 Left t1' => Left (Branch3 t1' k1 t2 k2 t3)

@@ -201,7 +201,7 @@ lookup _ Empty = Nothing

201lookup k (M _ t) = treeLookup k t

202

203insert : 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)

205insert k v (M _ t) =

206 case treeInsert k v t of

207 Left t' => (M _ t')

@@ -209,7 +209,7 @@ insert k v (M _ t) =

209

210delete : Ord k => k -> SortedMap k v -> SortedMap k v

211delete _ Empty = Empty

212−delete k (M O t) =

212+delete k (M Z t) =

213 case treeDelete k t of

214 Left t' => (M _ t')

215 Right () => Empty

lib/Data/Vect.idr+1−1

@@ -14,7 +14,7 @@ data Elem : a -> Vect a k -> Type where

14 There : {xs : Vect a k} -> Elem x xs -> Elem x (y::xs)

16findElem : 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

18findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))

20replaceElem : (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

24 show (NegS n) = "-" ++ show (S n)

26negZ : ZZ -> ZZ

27−negZ (Pos O) = Pos O

27+negZ (Pos Z) = Pos Z

28negZ (Pos (S n)) = NegS n

29negZ (NegS n) = Pos (S n)

31negNat : Nat -> ZZ

32−negNat O = Pos O

32+negNat Z = Pos Z

33negNat (S n) = NegS n

35minusNatZ : Nat -> Nat -> ZZ

36−minusNatZ n O = Pos n

36+minusNatZ n Z = Pos n

37−minusNatZ O (S m) = NegS m

37+minusNatZ Z (S m) = NegS m

38minusNatZ (S n) (S m) = minusNatZ n m

40plusZ : ZZ -> ZZ -> ZZ

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

101natMultZMult n m x h = cong h

102

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

104−doubleNegElim (Pos O) = refl

104+doubleNegElim (Pos Z) = refl

105doubleNegElim (Pos (S n)) = refl

106−doubleNegElim (NegS O) = refl

106+doubleNegElim (NegS Z) = refl

107doubleNegElim (NegS (S n)) = refl

108

109-- Injectivity

lib/Decidable/Equality.idr+4−4

@@ -41,13 +41,13 @@ instance DecEq Bool where

41-- Nat

42--------------------------------------------------------------------------------

44−total OnotS : O = S n -> _|_

44+total OnotS : Z = S n -> _|_

45OnotS refl impossible

47instance DecEq Nat where

48− decEq O O = Yes refl

48+ decEq Z Z = Yes refl

49− decEq O (S _) = No OnotS

49+ decEq Z (S _) = No OnotS

50− decEq (S _) O = No (negEqSym OnotS)

50+ decEq (S _) Z = No (negEqSym OnotS)

51 decEq (S n) (S m) with (decEq n m)

52 | Yes p = Yes $ cong p

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

55instance Poset Nat NatLTE where

56 antisymmetric = NatLTEIsAntisymmetric

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

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

59zeroNeverGreater {n} (nLTESm _) impossible

60zeroNeverGreater {n} nEqn impossible

@@ -66,8 +66,8 @@ nGTSm {n} {m} disprf (nEqn) impossible

67total

68decideNatLTE : (n : Nat) -> (m : Nat) -> Dec (NatLTE n m)

69−decideNatLTE O O = Yes nEqn

69+decideNatLTE Z Z = Yes nEqn

70−decideNatLTE (S x) O = No zeroNeverGreater

70+decideNatLTE (S x) Z = No zeroNeverGreater

71decideNatLTE x (S y) with (decEq x (S y))

72 | Yes eq = rewrite eq in Yes nEqn

73 | No _ with (decideNatLTE x y)

lib/Prelude.idr+1−1

@@ -251,7 +251,7 @@ instance Monad List where

251%lib C "m"

252

253pow : (Num a) => a -> Nat -> a

254−pow x O = 1

254+pow x Z = 1

255pow x (S n) = x * (pow x n)

256

257exp : Float -> Float

lib/Prelude/Fin.idr+3−3

@@ -17,7 +17,7 @@ finToNat fO a = a

17finToNat (fS x) a = finToNat x (S a)

19instance Cast (Fin n) Nat where

20− cast x = finToNat x O

20+ cast x = finToNat x Z

22finToInt : Fin n -> Integer -> Integer

23finToInt fO a = a

@@ -38,7 +38,7 @@ strengthen {n = S k} (fS i) with (strengthen i)

38strengthen f = Left f

40last : Fin (S n)

41−last {n=O} = fO

41+last {n=Z} = fO

42last {n=S _} = fS last

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

@@ -48,7 +48,7 @@ fSinjective refl = refl

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

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

51−natToFin O (S j) = Just fO

51+natToFin Z (S j) = Just fO

52natToFin (S k) (S j) with (natToFin k j)

53 | Just k' = Just (fS k')

54 | Nothing = Nothing

lib/Prelude/Heap.idr+2−2

@@ -27,7 +27,7 @@ isEmpty Empty = True

27isEmpty _ = False

29total size : MaxiphobicHeap a -> Nat

30−size Empty = O

30+size Empty = Z

31size (Node s l e r) = s

33isValidHeap : Ord a => MaxiphobicHeap a -> Bool

@@ -148,7 +148,7 @@ absurdBoolDischarge p = replace {P = disjointTy} p ()

148 disjointTy False = ()

149 disjointTy True = _|_

150

151−total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = O

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

152isEmptySizeZero Empty p = refl

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

154

lib/Prelude/List.idr+5−5

@@ -85,12 +85,12 @@ init' (x::xs) =

85--------------------------------------------------------------------------------

87take : Nat -> List a -> List a

88−take O xs = []

88+take Z xs = []

89take (S n) [] = []

90take (S n) (x::xs) = x :: take n xs

92drop : Nat -> List a -> List a

93−drop O xs = xs

93+drop Z xs = xs

94drop (S n) [] = []

95drop (S n) (x::xs) = drop n xs

@@ -127,7 +127,7 @@ repeat : a -> List a

127repeat x = x :: lazy (repeat x)

128

129replicate : Nat -> a -> List a

130−replicate O x = []

130+replicate Z x = []

131replicate (S n) x = x :: replicate n x

132

133--------------------------------------------------------------------------------

@@ -325,7 +325,7 @@ find p (x::xs) =

325 find p xs

326

327findIndex : (a -> Bool) -> List a -> Maybe Nat

328−findIndex = findIndex' O

328+findIndex = findIndex' Z

329 where

330-- findIndex' : Nat -> (a -> Bool) -> List a -> Maybe Nat

331 findIndex' cnt p [] = Nothing

@@ -336,7 +336,7 @@ findIndex = findIndex' O

336 findIndex' (S cnt) p xs

337

338findIndices : (a -> Bool) -> List a -> List Nat

339−findIndices = findIndices' O

339+findIndices = findIndices' Z

340 where

341-- findIndices' : Nat -> (a -> Bool) -> List a -> List Nat

342 findIndices' cnt p [] = []

lib/Prelude/Nat.idr+105−105

@@ -9,7 +9,7 @@ import Prelude.Cast

9%default total

11data Nat

12− = O

12+ = Z

13 | S Nat

15--------------------------------------------------------------------------------

@@ -17,11 +17,11 @@ data Nat

17--------------------------------------------------------------------------------

19total isZero : Nat -> Bool

20−isZero O = True

20+isZero Z = True

21isZero (S n) = False

23total isSucc : Nat -> Bool

24−isSucc O = False

24+isSucc Z = False

25isSucc (S n) = True

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

@@ -29,27 +29,27 @@ isSucc (S n) = True

29--------------------------------------------------------------------------------

31total plus : Nat -> Nat -> Nat

32−plus O right = right

32+plus Z right = right

33plus (S left) right = S (plus left right)

35total mult : Nat -> Nat -> Nat

36−mult O right = O

36+mult Z right = Z

37mult (S left) right = plus right $ mult left right

39total minus : Nat -> Nat -> Nat

40−minus O right = O

40+minus Z right = Z

41−minus left O = left

41+minus left Z = left

42minus (S left) (S right) = minus left right

44total power : Nat -> Nat -> Nat

45−power base O = S O

45+power base Z = S Z

46power base (S exp) = mult base $ power base exp

48hyper : Nat -> Nat -> Nat -> Nat

49−hyper O a b = S b

49+hyper Z a b = S b

50−hyper (S O) a O = a

50+hyper (S Z) a Z = a

51−hyper (S(S O)) a O = O

51+hyper (S(S Z)) a Z = Z

52−hyper n a O = S O

52+hyper n a Z = S Z

53hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)

@@ -58,7 +58,7 @@ hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)

58--------------------------------------------------------------------------------

60data LTE : Nat -> Nat -> Type where

61− lteZero : LTE O right

61+ lteZero : LTE Z right

62 lteSucc : LTE left right -> LTE (S left) (S right)

64total GTE : Nat -> Nat -> Type

@@ -71,8 +71,8 @@ total GT : Nat -> Nat -> Type

71GT left right = LT right left

73total lte : Nat -> Nat -> Bool

74−lte O right = True

74+lte Z right = True

75−lte left O = False

75+lte left Z = False

76lte (S left) (S right) = lte left right

78total gte : Nat -> Nat -> Bool

@@ -103,18 +103,18 @@ maximum left right =

103--------------------------------------------------------------------------------

104

105instance Eq Nat where

106− O == O = True

106+ Z == Z = True

107 (S l) == (S r) = l == r

108 _ == _ = False

109

110instance Cast Nat Integer where

111− cast O = 0

111+ cast Z = 0

112 cast (S k) = 1 + cast k

113

114instance Ord Nat where

115− compare O O = EQ

115+ compare Z Z = EQ

116− compare O (S k) = LT

116+ compare Z (S k) = LT

117− compare (S k) O = GT

117+ compare (S k) Z = GT

118 compare (S x) (S y) = compare x y

119

120instance Num Nat where

@@ -128,12 +128,12 @@ instance Num Nat where

128 where

129 %assert_total

130 fromInteger' : Integer -> Nat

131− fromInteger' 0 = O

131+ fromInteger' 0 = Z

132 fromInteger' n =

133 if (n > 0) then

134 S (fromInteger' (n - 1))

135 else

136− O

136+ Z

137

138instance Cast Integer Nat where

139 cast = fromInteger

@@ -171,10 +171,10 @@ instance Semigroup Additive where

171 getAdditive m => m

172

173instance Monoid Multiplicative where

174− neutral = getMultiplicative $ S O

174+ neutral = getMultiplicative $ S Z

175

176instance Monoid Additive where

177− neutral = getAdditive O

177+ neutral = getAdditive Z

178

179instance MeetSemilattice Nat where

180 meet = minimum

@@ -185,14 +185,14 @@ instance JoinSemilattice Nat where

185instance Lattice Nat where { }

186

187instance BoundedJoinSemilattice Nat where

188− bottom = O

188+ bottom = Z

189

190--------------------------------------------------------------------------------

191-- Auxilliary notions

192--------------------------------------------------------------------------------

193

194total pred : Nat -> Nat

195−pred O = O

195+pred Z = Z

196pred (S n) = n

197

198--------------------------------------------------------------------------------

@@ -200,8 +200,8 @@ pred (S n) = n

200--------------------------------------------------------------------------------

201

202total fib : Nat -> Nat

203−fib O = O

203+fib Z = Z

204−fib (S O) = S O

204+fib (S Z) = S Z

205fib (S (S n)) = fib (S n) + fib n

206

207--------------------------------------------------------------------------------

@@ -213,11 +213,11 @@ fib (S (S n)) = fib (S n) + fib n

213--------------------------------------------------------------------------------

214

215total mod : Nat -> Nat -> Nat

216−mod left O = left

216+mod left Z = left

217mod left (S right) = mod' left left right

218 where

219 total mod' : Nat -> Nat -> Nat -> Nat

220− mod' O centre right = centre

220+ mod' Z centre right = centre

221 mod' (S left) centre right =

222 if lte centre right then

223 centre

@@ -225,21 +225,21 @@ mod left (S right) = mod' left left right

225 mod' left (centre - (S right)) right

226

227total div : Nat -> Nat -> Nat

228−div left O = S left -- div by zero

228+div left Z = S left -- div by zero

229div left (S right) = div' left left right

230 where

231 total div' : Nat -> Nat -> Nat -> Nat

232− div' O centre right = O

232+ div' Z centre right = Z

233 div' (S left) centre right =

234 if lte centre right then

235− O

235+ Z

236 else

237 S (div' left (centre - (S right)) right)

238

239%assert_total

240log2 : Nat -> Nat

241−log2 O = O

241+log2 Z = Z

242−log2 (S O) = O

242+log2 (S Z) = Z

243log2 n = S (log2 (n `div` 2))

244

245--------------------------------------------------------------------------------

@@ -260,28 +260,28 @@ total plusZeroLeftNeutral : (right : Nat) -> 0 + right = right

260plusZeroLeftNeutral right = refl

261

262total plusZeroRightNeutral : (left : Nat) -> left + 0 = left

263−plusZeroRightNeutral O = refl

263+plusZeroRightNeutral Z = refl

264plusZeroRightNeutral (S n) =

265 let inductiveHypothesis = plusZeroRightNeutral n in

266 ?plusZeroRightNeutralStepCase

267

268total plusSuccRightSucc : (left : Nat) -> (right : Nat) ->

269 S (left + right) = left + (S right)

270−plusSuccRightSucc O right = refl

270+plusSuccRightSucc Z right = refl

271plusSuccRightSucc (S left) right =

272 let inductiveHypothesis = plusSuccRightSucc left right in

273 ?plusSuccRightSuccStepCase

274

275total plusCommutative : (left : Nat) -> (right : Nat) ->

276 left + right = right + left

277−plusCommutative O right = ?plusCommutativeBaseCase

277+plusCommutative Z right = ?plusCommutativeBaseCase

278plusCommutative (S left) right =

279 let inductiveHypothesis = plusCommutative left right in

280 ?plusCommutativeStepCase

281

282total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

283 left + (centre + right) = (left + centre) + right

284−plusAssociative O centre right = refl

284+plusAssociative Z centre right = refl

285plusAssociative (S left) centre right =

286 let inductiveHypothesis = plusAssociative left centre right in

287 ?plusAssociativeStepCase

@@ -299,38 +299,38 @@ plusOneSucc n = refl

299

300total plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->

301 (p : left + right = left + right') -> right = right'

302−plusLeftCancel O right right' p = ?plusLeftCancelBaseCase

302+plusLeftCancel Z right right' p = ?plusLeftCancelBaseCase

303plusLeftCancel (S left) right right' p =

304 let inductiveHypothesis = plusLeftCancel left right right' in

305 ?plusLeftCancelStepCase

306

307total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->

308 (p : left + right = left' + right) -> left = left'

309−plusRightCancel left left' O p = ?plusRightCancelBaseCase

309+plusRightCancel left left' Z p = ?plusRightCancelBaseCase

310plusRightCancel left left' (S right) p =

311 let inductiveHypothesis = plusRightCancel left left' right in

312 ?plusRightCancelStepCase

313

314total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->

315− (p : left + right = left) -> right = O

315+ (p : left + right = left) -> right = Z

316−plusLeftLeftRightZero O right p = ?plusLeftLeftRightZeroBaseCase

316+plusLeftLeftRightZero Z right p = ?plusLeftLeftRightZeroBaseCase

317plusLeftLeftRightZero (S left) right p =

318 let inductiveHypothesis = plusLeftLeftRightZero left right in

319 ?plusLeftLeftRightZeroStepCase

320

321-- Mult

322−total multZeroLeftZero : (right : Nat) -> O * right = O

322+total multZeroLeftZero : (right : Nat) -> Z * right = Z

323multZeroLeftZero right = refl

324

325−total multZeroRightZero : (left : Nat) -> left * O = O

325+total multZeroRightZero : (left : Nat) -> left * Z = Z

326−multZeroRightZero O = refl

326+multZeroRightZero Z = refl

327multZeroRightZero (S left) =

328 let inductiveHypothesis = multZeroRightZero left in

329 ?multZeroRightZeroStepCase

330

331total multRightSuccPlus : (left : Nat) -> (right : Nat) ->

332 left * (S right) = left + (left * right)

333−multRightSuccPlus O right = refl

333+multRightSuccPlus Z right = refl

334multRightSuccPlus (S left) right =

335 let inductiveHypothesis = multRightSuccPlus left right in

336 ?multRightSuccPlusStepCase

@@ -341,40 +341,40 @@ multLeftSuccPlus left right = refl

341

342total multCommutative : (left : Nat) -> (right : Nat) ->

343 left * right = right * left

344−multCommutative O right = ?multCommutativeBaseCase

344+multCommutative Z right = ?multCommutativeBaseCase

345multCommutative (S left) right =

346 let inductiveHypothesis = multCommutative left right in

347 ?multCommutativeStepCase

348

349total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

350 left * (centre + right) = (left * centre) + (left * right)

351−multDistributesOverPlusRight O centre right = refl

351+multDistributesOverPlusRight Z centre right = refl

352multDistributesOverPlusRight (S left) centre right =

353 let inductiveHypothesis = multDistributesOverPlusRight left centre right in

354 ?multDistributesOverPlusRightStepCase

355

356total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

357 (left + centre) * right = (left * right) + (centre * right)

358−multDistributesOverPlusLeft O centre right = refl

358+multDistributesOverPlusLeft Z centre right = refl

359multDistributesOverPlusLeft (S left) centre right =

360 let inductiveHypothesis = multDistributesOverPlusLeft left centre right in

361 ?multDistributesOverPlusLeftStepCase

362

363total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

364 left * (centre * right) = (left * centre) * right

365−multAssociative O centre right = refl

365+multAssociative Z centre right = refl

366multAssociative (S left) centre right =

367 let inductiveHypothesis = multAssociative left centre right in

368 ?multAssociativeStepCase

369

370total multOneLeftNeutral : (right : Nat) -> 1 * right = right

371−multOneLeftNeutral O = refl

371+multOneLeftNeutral Z = refl

372multOneLeftNeutral (S right) =

373 let inductiveHypothesis = multOneLeftNeutral right in

374 ?multOneLeftNeutralStepCase

375

376total multOneRightNeutral : (left : Nat) -> left * 1 = left

377−multOneRightNeutral O = refl

377+multOneRightNeutral Z = refl

378multOneRightNeutral (S left) =

379 let inductiveHypothesis = multOneRightNeutral left in

380 ?multOneRightNeutralStepCase

@@ -384,51 +384,51 @@ total minusSuccSucc : (left : Nat) -> (right : Nat) ->

384 (S left) - (S right) = left - right

385minusSuccSucc left right = refl

386

387−total minusZeroLeft : (right : Nat) -> 0 - right = O

387+total minusZeroLeft : (right : Nat) -> 0 - right = Z

388minusZeroLeft right = refl

389

390total minusZeroRight : (left : Nat) -> left - 0 = left

391−minusZeroRight O = refl

391+minusZeroRight Z = refl

392minusZeroRight (S left) = refl

393

394−total minusZeroN : (n : Nat) -> O = n - n

394+total minusZeroN : (n : Nat) -> Z = n - n

395−minusZeroN O = refl

395+minusZeroN Z = refl

396minusZeroN (S n) = minusZeroN n

397

398−total minusOneSuccN : (n : Nat) -> S O = (S n) - n

398+total minusOneSuccN : (n : Nat) -> S Z = (S n) - n

399−minusOneSuccN O = refl

399+minusOneSuccN Z = refl

400minusOneSuccN (S n) = minusOneSuccN n

401

402total minusSuccOne : (n : Nat) -> S n - 1 = n

403−minusSuccOne O = refl

403+minusSuccOne Z = refl

404minusSuccOne (S n) = refl

405

406−total minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = O

406+total minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = Z

407−minusPlusZero O m = refl

407+minusPlusZero Z m = refl

408minusPlusZero (S n) m = minusPlusZero n m

409

410total minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

411 left - centre - right = left - (centre + right)

412−minusMinusMinusPlus O O right = refl

412+minusMinusMinusPlus Z Z right = refl

413−minusMinusMinusPlus (S left) O right = refl

413+minusMinusMinusPlus (S left) Z right = refl

414−minusMinusMinusPlus O (S centre) right = refl

414+minusMinusMinusPlus Z (S centre) right = refl

415minusMinusMinusPlus (S left) (S centre) right =

416 let inductiveHypothesis = minusMinusMinusPlus left centre right in

417 ?minusMinusMinusPlusStepCase

418

419total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->

420 (left + right) - (left + right') = right - right'

421−plusMinusLeftCancel O right right' = refl

421+plusMinusLeftCancel Z right right' = refl

422plusMinusLeftCancel (S left) right right' =

423 let inductiveHypothesis = plusMinusLeftCancel left right right' in

424 ?plusMinusLeftCancelStepCase

425

426total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

427 (left - centre) * right = (left * right) - (centre * right)

428−multDistributesOverMinusLeft O O right = refl

428+multDistributesOverMinusLeft Z Z right = refl

429−multDistributesOverMinusLeft (S left) O right =

429+multDistributesOverMinusLeft (S left) Z right =

430 ?multDistributesOverMinusLeftBaseCase

431−multDistributesOverMinusLeft O (S centre) right = refl

431+multDistributesOverMinusLeft Z (S centre) right = refl

432multDistributesOverMinusLeft (S left) (S centre) right =

433 let inductiveHypothesis = multDistributesOverMinusLeft left centre right in

434 ?multDistributesOverMinusLeftStepCase

@@ -445,35 +445,35 @@ powerSuccPowerLeft base exp = refl

445

446total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->

447 (power base exp) * (power base exp') = power base (exp + exp')

448−multPowerPowerPlus base O exp' = ?multPowerPowerPlusBaseCase

448+multPowerPowerPlus base Z exp' = ?multPowerPowerPlusBaseCase

449multPowerPowerPlus base (S exp) exp' =

450 let inductiveHypothesis = multPowerPowerPlus base exp exp' in

451 ?multPowerPowerPlusStepCase

452

453−total powerZeroOne : (base : Nat) -> power base 0 = S O

453+total powerZeroOne : (base : Nat) -> power base 0 = S Z

454powerZeroOne base = refl

455

456total powerOneNeutral : (base : Nat) -> power base 1 = base

457−powerOneNeutral O = refl

457+powerOneNeutral Z = refl

458powerOneNeutral (S base) =

459 let inductiveHypothesis = powerOneNeutral base in

460 ?powerOneNeutralStepCase

461

462−total powerOneSuccOne : (exp : Nat) -> power 1 exp = S O

462+total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z

463−powerOneSuccOne O = refl

463+powerOneSuccOne Z = refl

464powerOneSuccOne (S exp) =

465 let inductiveHypothesis = powerOneSuccOne exp in

466 ?powerOneSuccOneStepCase

467

468total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base

469−powerSuccSuccMult O = refl

469+powerSuccSuccMult Z = refl

470powerSuccSuccMult (S base) =

471 let inductiveHypothesis = powerSuccSuccMult base in

472 ?powerSuccSuccMultStepCase

473

474total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->

475 power (power base exp) exp' = power base (exp * exp')

476−powerPowerMultPower base exp O = ?powerPowerMultPowerBaseCase

476+powerPowerMultPower base exp Z = ?powerPowerMultPowerBaseCase

477powerPowerMultPower base exp (S exp') =

478 let inductiveHypothesis = powerPowerMultPower base exp exp' in

479 ?powerPowerMultPowerStepCase

@@ -484,9 +484,9 @@ predSucc n = refl

484

485total minusSuccPred : (left : Nat) -> (right : Nat) ->

486 left - (S right) = pred (left - right)

487−minusSuccPred O right = refl

487+minusSuccPred Z right = refl

488−minusSuccPred (S left) O =

488+minusSuccPred (S left) Z =

489− let inductiveHypothesis = minusSuccPred left O in

489+ let inductiveHypothesis = minusSuccPred left Z in

490 ?minusSuccPredStepCase

491minusSuccPred (S left) (S right) =

492 let inductiveHypothesis = minusSuccPred left right in

@@ -520,69 +520,69 @@ boolElimMultMultRight False right t f = refl

520

521-- Orders

522total lteNTrue : (n : Nat) -> lte n n = True

523−lteNTrue O = refl

523+lteNTrue Z = refl

524lteNTrue (S n) = lteNTrue n

525

526−total lteSuccZeroFalse : (n : Nat) -> lte (S n) O = False

526+total lteSuccZeroFalse : (n : Nat) -> lte (S n) Z = False

527−lteSuccZeroFalse O = refl

527+lteSuccZeroFalse Z = refl

528lteSuccZeroFalse (S n) = refl

529

530-- Minimum and maximum

531−total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = O

531+total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z

532−minimumZeroZeroRight O = refl

532+minimumZeroZeroRight Z = refl

533minimumZeroZeroRight (S right) = minimumZeroZeroRight right

534

535−total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = O

535+total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z

536−minimumZeroZeroLeft O = refl

536+minimumZeroZeroLeft Z = refl

537minimumZeroZeroLeft (S left) = refl

538

539total minimumSuccSucc : (left : Nat) -> (right : Nat) ->

540 minimum (S left) (S right) = S (minimum left right)

541−minimumSuccSucc O O = refl

541+minimumSuccSucc Z Z = refl

542−minimumSuccSucc (S left) O = refl

542+minimumSuccSucc (S left) Z = refl

543−minimumSuccSucc O (S right) = refl

543+minimumSuccSucc Z (S right) = refl

544minimumSuccSucc (S left) (S right) =

545 let inductiveHypothesis = minimumSuccSucc left right in

546 ?minimumSuccSuccStepCase

547

548total minimumCommutative : (left : Nat) -> (right : Nat) ->

549 minimum left right = minimum right left

550−minimumCommutative O O = refl

550+minimumCommutative Z Z = refl

551−minimumCommutative O (S right) = refl

551+minimumCommutative Z (S right) = refl

552−minimumCommutative (S left) O = refl

552+minimumCommutative (S left) Z = refl

553minimumCommutative (S left) (S right) =

554 let inductiveHypothesis = minimumCommutative left right in

555 ?minimumCommutativeStepCase

556

557−total maximumZeroNRight : (right : Nat) -> maximum O right = right

557+total maximumZeroNRight : (right : Nat) -> maximum Z right = right

558−maximumZeroNRight O = refl

558+maximumZeroNRight Z = refl

559maximumZeroNRight (S right) = refl

560

561−total maximumZeroNLeft : (left : Nat) -> maximum left O = left

561+total maximumZeroNLeft : (left : Nat) -> maximum left Z = left

562−maximumZeroNLeft O = refl

562+maximumZeroNLeft Z = refl

563maximumZeroNLeft (S left) = refl

564

565total maximumSuccSucc : (left : Nat) -> (right : Nat) ->

566 S (maximum left right) = maximum (S left) (S right)

567−maximumSuccSucc O O = refl

567+maximumSuccSucc Z Z = refl

568−maximumSuccSucc (S left) O = refl

568+maximumSuccSucc (S left) Z = refl

569−maximumSuccSucc O (S right) = refl

569+maximumSuccSucc Z (S right) = refl

570maximumSuccSucc (S left) (S right) =

571 let inductiveHypothesis = maximumSuccSucc left right in

572 ?maximumSuccSuccStepCase

573

574total maximumCommutative : (left : Nat) -> (right : Nat) ->

575 maximum left right = maximum right left

576−maximumCommutative O O = refl

576+maximumCommutative Z Z = refl

577−maximumCommutative (S left) O = refl

577+maximumCommutative (S left) Z = refl

578−maximumCommutative O (S right) = refl

578+maximumCommutative Z (S right) = refl

579maximumCommutative (S left) (S right) =

580 let inductiveHypothesis = maximumCommutative left right in

581 ?maximumCommutativeStepCase

582

583-- div and mod

584−total modZeroZero : (n : Nat) -> mod 0 n = O

584+total modZeroZero : (n : Nat) -> mod 0 n = Z

585−modZeroZero O = refl

585+modZeroZero Z = refl

586modZeroZero (S n) = refl

587

588--------------------------------------------------------------------------------

@@ -613,7 +613,7 @@ powerSuccSuccMultStepCase = proof {

613powerOneSuccOneStepCase = proof {

614 intros;

615 rewrite inductiveHypothesis;

616− rewrite sym (plusZeroRightNeutral (power (S O) exp));

616+ rewrite sym (plusZeroRightNeutral (power (S Z) exp));

617 trivial;

618}

619

lib/Prelude/Vect.idr+3−3

@@ -10,7 +10,7 @@ import Prelude.Nat

10infixr 7 ::

12data Vect : Type -> Nat -> Type where

13− Nil : Vect a O

13+ Nil : Vect a Z

14 (::) : a -> Vect a n -> Vect a (S n)

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

@@ -81,7 +81,7 @@ fromList (x::xs) = x :: fromList xs

81(++) (x::xs) ys = x :: xs ++ ys

83replicate : (n : Nat) -> a -> Vect a n

84−replicate O x = []

84+replicate Z x = []

85replicate (S k) x = x :: replicate k x

87--------------------------------------------------------------------------------

@@ -322,7 +322,7 @@ range =

322 reverse range_

323 where

324 range_ : Vect (Fin n) n

325− range_ {n=O} = Nil

325+ range_ {n=Z} = Nil

326 range_ {n=(S _)} = last :: map weaken range_

327

328--------------------------------------------------------------------------------

lib/Uninhabited.idr+2−2

@@ -3,10 +3,10 @@ module Uninhabited

3class Uninhabited t where

4 total uninhabited : t -> _|_

6−instance Uninhabited (Fin O) where

6+instance Uninhabited (Fin Z) where

7 uninhabited fO impossible

8 uninhabited (fS f) impossible

10−instance Uninhabited (O = S n) where

10+instance Uninhabited (Z = S n) where

11 uninhabited refl impossible

samples/binary.idr+2−2

@@ -11,7 +11,7 @@ instance Show (Bit n) where

11infixl 5 #

13data Binary : (width : Nat) -> (value : Nat) -> Type where

14− zero : Binary O O

14+ zero : Binary Z Z

15 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)

17instance Show (Binary w k) where

@@ -83,7 +83,7 @@ main.adc_lemma_2 = proof {

83 rewrite sym (plusAssociative x v v1);

84 rewrite sym (plusCommutative (plus (plus x v) v1) v1);

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

87 trivial;

88}

src/IRTS/Compiler.hs+3−3

@@ -237,7 +237,7 @@ instance ToIR (TT Name) where

237 where mkUnused u i [] = []

238 mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs

239 | 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"]) _)

241-- = return $ LConst (BI 0)

242 ir' env (P _ n _) = return $ LV (Glob n)

243 ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))

@@ -331,7 +331,7 @@ mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))

331mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))

332mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))

333

334−zname = NS (UN "O") ["Nat","Prelude"]

334+zname = NS (UN "Z") ["Nat","Prelude"]

335sname = NS (UN "S") ["Nat","Prelude"]

336

337instance ToIR ([Name], SC) where

@@ -351,7 +351,7 @@ instance ToIR SC where

351 return $ LCase (LV (Glob n)) alts'

352 ir' ImpossibleCase = return LNothing

353

354− -- special cases for O and S

354+ -- special cases for Z and S

355 -- Needs rethink: projections make this fail

356-- mkIRAlt n (ConCase z _ [] rhs) | z == zname

357-- = mkIRAlt n (ConstCase (BI 0) rhs)

src/Idris/AbsSyntaxTree.hs+2−2

@@ -1128,10 +1128,10 @@ showImp impl tm = se 10 tm where

1128 xs -> "[" ++ intercalate "," (map (se p) xs) ++ "]"

1129 slist _ _ = Nothing

1130

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

1132 -- Nat ones.

1133 snat p (PRef _ o)

1134− | show o == (natns++"O") || show o == "O" = Just 0

1134+ | show o == (natns++"Z") || show o == "Z" = Just 0

1135 snat p (PApp _ s [PExp {getTm=n}])

1136 | show s == (natns++"S") || show s == "S",

1137 Just n' <- snat p n

src/Idris/Transforms.hs+1−1

@@ -39,7 +39,7 @@ instance Transform CaseAlt where

40natTrans = [TermTrans zero, TermTrans suc, CaseTrans natcase]

42−zname = NS (UN "O") ["Nat","Prelude"]

42+zname = NS (UN "Z") ["Nat","Prelude"]

43sname = NS (UN "S") ["Nat","Prelude"]

45zero :: TT Name -> TT Name

test/reg001/reg001.idr+1−1

@@ -8,4 +8,4 @@ data Imp : Type where

8 MkImp : {any : Type} -> any -> Imp

10testVal : 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

3h : Bool -> Nat

4h False = r1 where

5 r : Nat

6− r = S O

6+ r = S Z

7 r1 : Nat

8 r1 = r

9h True = r2 where

10 r : Nat

11− r = O

11+ r = Z

12 r2 : Nat

13 r2 = r

test/reg005/reg005.idr+3−3

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

1module Main

3rep : (n : Nat) -> Char -> Vect Char n

4−rep O x = []

4+rep Z x = []

5rep (S k) x = x :: rep k x

7data RLE : Vect Char n -> Type where

@@ -18,12 +18,12 @@ eq x y = if x == y then Just ?eqCharOK else Nothing

18rle : (xs : Vect Char n) -> RLE xs

19rle [] = REnd

20rle (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

22 rle (x :: rep (S n) yvar ++ ys) | RChar n yvar rs with (eq x yvar)

23 rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just refl

24 = RChar (S n) x rs

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

28compress : Vect Char n -> String

29compress xs with (rle xs)

test/reg006/reg006.idr+1−1

@@ -3,7 +3,7 @@ module RBTree

3data Colour = Red | Black

5data RBTree : Type -> Type -> Nat -> Colour -> Type where

6− Leaf : RBTree k v O Black

6+ Leaf : RBTree k v Z Black

7 RedBranch : k -> v -> RBTree k v n Black -> RBTree k v n Black -> RBTree k v n Red

8 BlackBranch : k -> v -> RBTree k v n x -> RBTree k v n y -> RBTree k v (S n) Black

test/reg008/reg008.idr+3−3

@@ -6,9 +6,9 @@ data Cmp : Nat -> Nat -> Type where

6 cmpGT : (x : _) -> Cmp (y + S x) y

8total cmp : (x, y : Nat) -> Cmp x y

9−cmp O O = cmpEQ

9+cmp Z Z = cmpEQ

10−cmp O (S k) = cmpLT _

10+cmp Z (S k) = cmpLT _

11−cmp (S k) O = cmpGT _

11+cmp (S k) Z = cmpGT _

12cmp (S x) (S y) with (cmp x y)

13 cmp (S x) (S (x + (S k))) | cmpLT k = cmpLT k

14 cmp (S x) (S x) | cmpEQ = cmpEQ

test/reg009/reg009.lidr+1−1

@@ -6,7 +6,7 @@

6> filterTagP : (p : alpha -> Bool) ->

7> (as : Vect alpha n) ->

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

10> filterTagP {n = S m} p (a :: as) q with (p a)

11> | True = (_

12> **

test/reg010/reg010.idr+1−1

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

1module usubst

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

5 unsafeSubst P x x px | _ = px

test/reg011/reg011.idr+2−2

@@ -1,9 +1,9 @@

1vfoldl : (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

3 -> Vect a m -> P m

4-- vfoldl P cons nil []

5-- = nil

6vfoldl 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

8-- vfoldl P cons nil (x :: xs)

9-- = vfoldl (\n => P (S n)) (\ n => cons _) (cons _ nil x) xs

test/reg018/reg018b.idr+3−3

@@ -2,13 +2,13 @@ module A

3%default total

5−codata B = O B | I B

5+codata B = Z B | I B

7showB : B -> String

8showB (I x) = "I" ++ showB x

9−showB (O x) = "O" ++ showB x

9+showB (Z x) = "Z" ++ showB x

11instance Show B where show = showB

13os : 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)

9-- natFromStream n = (::) n (natFromStream (S n))

11take : (n: Nat) -> InfStream a -> Vect a n

12−take O _ = []

12+take Z _ = []

13take (S n) (x :: xs) = x :: take n xs

15hdtl : InfStream a -> (a, InfStream a)

test/reg018/reg018d.idr+1−1

@@ -2,7 +2,7 @@ module Main

3total

4pull : 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)

6-- pull {n=S q} fO (Vect.(::) {n=S _} x xs) = (x, xs)

7pull {n=S _} (fS n) (x :: xs) =

8 let (v, vs) = pull n xs in

test/test005/test005.idr+1−1

@@ -8,7 +8,7 @@ tlist = [1, 2, 3, 4, 5]

9main : IO ()

10main = do print (abs (-8))

11− print (abs (S O))

11+ print (abs (S Z))

12 print (span isAlpha tstr)

13 print (break isDigit tstr)

14 print (span (\x => x < 3) tlist)

test/test006/test006.idr+3−3

@@ -5,14 +5,14 @@ data Parity : Nat -> Type where

5 odd : Parity (S (n + n))

7parity : (n:Nat) -> Parity n

8−parity O = even {n=O}

8+parity Z = even {n=Z}

9−parity (S O) = odd {n=O}

9+parity (S Z) = odd {n=Z}

10parity (S (S k)) with (parity k)

11 parity (S (S (j + j))) | (even {n = j}) ?= even {n=S j}

12 parity (S (S (S (j + j)))) | (odd {n = j}) ?= odd {n=S j}

14natToBin : Nat -> List Bool

15−natToBin O = Nil

15+natToBin Z = Nil

16natToBin k with (parity k)

17 natToBin (j + j) | even {n = j} = False :: natToBin j

18 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

5 odd : Parity (S (n + n))

7parity : (n:Nat) -> Parity n

8−parity O = even {n=O}

8+parity Z = even {n=Z}

9−parity (S O) = odd {n=O}

9+parity (S Z) = odd {n=Z}

10parity (S (S k)) with (parity k)

11 parity (S (S (j + j))) | even ?= even {n=S j}

12 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}

test/test015/test015.idr+6−6

@@ -4,8 +4,8 @@ import Parity

4import System

6data Bit : Nat -> Type where

7− b0 : Bit O

7+ b0 : Bit Z

8− b1 : Bit (S O)

8+ b1 : Bit (S Z)

10instance Show (Bit n) where

11 show = show' where

@@ -16,7 +16,7 @@ instance Show (Bit n) where

16infixl 5 #

18data Binary : (width : Nat) -> (value : Nat) -> Type where

19− zero : Binary O O

19+ zero : Binary Z Z

20 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)

22instance Show (Binary w k) where

@@ -29,9 +29,9 @@ pad (num # x) = pad num # x

30natToBin : (width : Nat) -> (n : Nat) ->

31 Maybe (Binary width n)

32−natToBin O (S k) = Nothing

32+natToBin Z (S k) = Nothing

33−natToBin O O = Just zero

33+natToBin Z Z = Just zero

34−natToBin (S k) O = do x <- natToBin k O

34+natToBin (S k) Z = do x <- natToBin k Z

35 Just (pad x)

36natToBin (S w) (S k) with (parity k)

37 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

8countFrom x = x :: countFrom (x + 1)

10take : Nat -> Stream a -> List a

11−take O _ = []

11+take Z _ = []

12take (S n) (x :: xs) = x :: take n xs

13take n [] = []

test/test017/test017.idr+16−16

@@ -5,8 +5,8 @@ module scg

5data Ord = Zero | Suc Ord | Sup (Nat -> Ord)

7natElim : (n : Nat) -> (P : Nat -> Type) ->

8− (P O) -> ((n : Nat) -> (P n) -> (P (S n))) -> (P n)

8+ (P Z) -> ((n : Nat) -> (P n) -> (P (S n))) -> (P n)

9−natElim O P mO mS = mO

9+natElim Z P mO mS = mO

10natElim (S k) P mO mS = mS k (natElim k P mO mS)

12ordElim : (x : Ord) ->

@@ -23,10 +23,10 @@ ordElim (Sup f) P mZ mSuc mSup =

23myplus' : Nat -> Nat -> Nat

24myplus : Nat -> Nat -> Nat

26−myplus O y = y

26+myplus Z y = y

27myplus (S k) y = S (myplus' k y)

29−myplus' O y = y

29+myplus' Z y = y

30myplus' (S k) y = S (myplus y k)

32mnubBy : (a -> a -> Bool) -> List a -> List a

@@ -46,23 +46,23 @@ vtrans [] _ = []

46vtrans (x :: xs) ys = x :: vtrans ys ys

48even : Nat -> Bool

49−even O = True

49+even Z = True

50even (S k) = odd k

51 where

52 odd : Nat -> Bool

53− odd O = False

53+ odd Z = False

54 odd (S k) = even k

56ack : Nat -> Nat -> Nat

57−ack O n = S n

57+ack Z n = S n

58−ack (S m) O = ack m (S O)

58+ack (S m) Z = ack m (S Z)

59ack (S m) (S n) = ack m (ack (S m) n)

61data Bin = eps | c0 Bin | c1 Bin

63foo : Bin -> Nat

64−foo eps = O

64+foo eps = Z

65−foo (c0 eps) = O

65+foo (c0 eps) = Z

66foo (c0 (c1 x)) = S (foo (c1 x))

67foo (c0 (c0 x)) = foo (c0 x)

68foo (c1 x) = S (foo x)

@@ -70,19 +70,19 @@ foo (c1 x) = S (foo x)

70bar : Nat -> Nat -> Nat

71bar x y = mp x y where

72 mp : Nat -> Nat -> Nat

73− mp O y = y

73+ mp Z y = y

74 mp (S k) y = S (bar k y)

76total mfib : Nat -> Nat

77−mfib O = O

77+mfib Z = Z

78−mfib (S O) = S O

78+mfib (S Z) = S Z

79mfib (S (S n)) = mfib (S n) + mfib n

81maxCommutative : (left : Nat) -> (right : Nat) ->

82 maximum left right = maximum right left

83−maxCommutative O O = refl

83+maxCommutative Z Z = refl

84−maxCommutative (S left) O = refl

84+maxCommutative (S left) Z = refl

85−maxCommutative O (S right) = refl

85+maxCommutative Z (S right) = refl

86maxCommutative (S left) (S right) =

87 let inductiveHypothesis = maxCommutative left right in

88 ?maxCommutativeStepCase

test/test019/test019.lidr+1−1

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

1> module Main

3> ifTrue : so True -> Nat

4−> ifTrue oh = S O

4+> ifTrue oh = S Z

6> ifFalse : so False -> Nat

7> ifFalse oh impossible

test/test025/test025.idr+2−2

@@ -21,9 +21,9 @@ testMemory = do Src :- allocate 5

21 Dst :- initialize (prim__truncInt_B8 1) 2 oh

22 move 2 2 3 oh oh

23 Src :- free

24− end <- Dst :- peek 4 (S O) 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 O)))) oh

26+ res <- Dst :- peek 1 (S(S(S(S Z)))) oh

27 Dst :- free

28 return (map (prim__zextB8_Int) res)

tutorial/classes.tex+8−8

@@ -43,10 +43,10 @@ could be defined as:

43\begin{SaveVerbatim}{shownat}

45instance Show Nat where

46− show O = "O"

46+ show Z = "Z"

47 show (S k) = "s" ++ show k

49−Idris> show (S (S (S O)))

49+Idris> show (S (S (S Z)))

50"sssO" : String

52\end{SaveVerbatim}

@@ -101,10 +101,10 @@ For example, for an instance of \texttt{Eq} for \texttt{Nat}:

101\begin{SaveVerbatim}{eqnat}

102

103instance Eq Nat where

104− O == O = True

104+ Z == Z = True

105 (S x) == (S y) = x == y

106− O == (S y) = False

106+ Z == (S y) = False

107− (S x) == O = False

107+ (S x) == Z = False

108

109 x /= y = not (x == y)

110

@@ -498,9 +498,9 @@ be \remph{named} as follows:

498\begin{SaveVerbatim}{myord}

499

500instance [myord] Ord Nat where

501− compare O (S n) = GT

501+ compare Z (S n) = GT

502− compare (S n) O = LT

502+ compare (S n) Z = LT

503− compare O O = EQ

503+ compare Z Z = EQ

504 compare (S x) (S y) = compare @{myord} x y

505

506\end{SaveVerbatim}

tutorial/examples/binary.idr+6−6

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

1module Main

3data Binary : Nat -> Type where

4− bEnd : Binary O

4+ bEnd : Binary Z

5 bO : Binary n -> Binary (n + n)

6 bI : Binary n -> Binary (S (n + n))

@@ -15,21 +15,21 @@ data Parity : Nat -> Type where

15 odd : Parity (S (n + n))

17parity : (n:Nat) -> Parity n

18−parity O = even {n=O}

18+parity Z = even {n=Z}

19−parity (S O) = odd {n=O}

19+parity (S Z) = odd {n=Z}

20parity (S (S k)) with (parity k)

21 parity (S (S (j + j))) | even ?= even {n=S j}

22 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}

24natToBin : (n:Nat) -> Binary n

25−natToBin O = bEnd

25+natToBin Z = bEnd

26natToBin (S k) with (parity k)

27 natToBin (S (j + j)) | even = bI (natToBin j)

28 natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))

30intToNat : Int -> Nat

31−intToNat 0 = O

31+intToNat 0 = Z

32−intToNat x = if (x>0) then (S (intToNat (x-1))) else O

32+intToNat x = if (x>0) then (S (intToNat (x-1))) else Z

34main : IO ()

35main = do putStr "Enter a number: "

tutorial/examples/theorems.idr+14−14

@@ -5,15 +5,15 @@ fiveIsFive = refl

5twoPlusTwo : 2 + 2 = 4

6twoPlusTwo = refl

8−total disjoint : (n : Nat) -> O = S n -> _|_

8+total disjoint : (n : Nat) -> Z = S n -> _|_

9disjoint n p = replace {P = disjointTy} p ()

10 where

11 disjointTy : Nat -> Type

12− disjointTy O = ()

12+ disjointTy Z = ()

13 disjointTy (S k) = _|_

15total acyclic : (n : Nat) -> n = S n -> _|_

16−acyclic O p = disjoint _ p

16+acyclic Z p = disjoint _ p

17acyclic (S k) p = acyclic k (succInjective _ _ p)

19empty1 : _|_

@@ -24,33 +24,33 @@ empty1 = hd [] where

24empty2 : _|_

25empty2 = empty2

27−plusReduces : (n:Nat) -> plus O n = n

27+plusReduces : (n:Nat) -> plus Z n = n

28plusReduces n = refl

30−plusReducesO : (n:Nat) -> n = plus n O

30+plusReducesZ : (n:Nat) -> n = plus n Z

31−plusReducesO O = refl

31+plusReducesZ Z = refl

32−plusReducesO (S k) = cong (plusReducesO k)

32+plusReducesZ (S k) = cong (plusReducesZ k)

34plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)

35−plusReducesS O m = refl

35+plusReducesS Z m = refl

36plusReducesS (S k) m = cong (plusReducesS k m)

38−plusReducesO' : (n:Nat) -> n = plus n O

38+plusReducesZ' : (n:Nat) -> n = plus n Z

39−plusReducesO' O = ?plusredO_O

39+plusReducesZ' Z = ?plusredZ_Z

40−plusReducesO' (S k) = let ih = plusReducesO' k in

40+plusReducesZ' (S k) = let ih = plusReducesZ' k in

41− ?plusredO_S

41+ ?plusredZ_S

44---------- Proofs ----------

46−plusredO_S = proof {

46+plusredZ_S = proof {

47 intro;

48 intro;

49 rewrite ih;

50 trivial;

51}

53−plusredO_O = proof {

53+plusredZ_Z = proof {

54 compute;

55 trivial;

56}

tutorial/examples/usefultypes.idr+1−1

@@ -10,7 +10,7 @@ vec = (_ ** [3, 4])

11list_lookup : Nat -> List a -> Maybe a

12list_lookup _ Nil = Nothing

13−list_lookup O (x :: xs) = Just x

13+list_lookup Z (x :: xs) = Just x

14list_lookup (S k) (x :: xs) = list_lookup k xs

16lookup_default : Nat -> List a -> a -> a

tutorial/examples/views.idr+3−3

@@ -5,14 +5,14 @@ data Parity : Nat -> Type where

5 odd : Parity (S (n + n))

7parity : (n:Nat) -> Parity n

8−parity O = even {n=O}

8+parity Z = even {n=Z}

9−parity (S O) = odd {n=O}

9+parity (S Z) = odd {n=Z}

10parity (S (S k)) with (parity k)

11 parity (S (S (j + j))) | even ?= even {n=S j}

12 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}

14natToBin : Nat -> List Bool

15−natToBin O = Nil

15+natToBin Z = Nil

16natToBin k with (parity k)

17 natToBin (j + j) | even = False :: natToBin j

18 natToBin (S (j + j)) | odd = True :: natToBin j

tutorial/examples/wheres.idr+3−3

@@ -1,13 +1,13 @@

1module wheres

3even : Nat -> Bool

4−even O = True

4+even Z = True

5even (S k) = odd k where

6− odd O = False

6+ odd Z = False

7 odd (S k) = even k

9test : List Nat

10−test = [c (S 1), c O, d (S O)]

10+test = [c (S 1), c Z, d (S Z)]

11 where c x = 42 + x

12 d y = c (y + 1 + z y)

13 where z w = y + w

tutorial/provisional.tex+6−6

@@ -22,8 +22,8 @@ We'd like to implement this as follows:

22\begin{SaveVerbatim}{parfail}

24parity : (n:Nat) -> Parity n

25−parity O = even {n=O}

25+parity Z = even {n=Z}

26−parity (S O) = odd {n=O}

26+parity (S Z) = odd {n=Z}

27parity (S (S k)) with (parity k)

28 parity (S (S (j + j))) | even = even {n=S j}

29 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

77\begin{SaveVerbatim}{paritypro}

79parity : (n:Nat) -> Parity n

80−parity O = even {n=O}

80+parity Z = even {n=Z}

81−parity (S O) = odd {n=O}

81+parity (S Z) = odd {n=Z}

82parity (S (S k)) with (parity k)

83 parity (S (S (j + j))) | even ?= even {n=S j}

84 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}

@@ -231,7 +231,7 @@ case \texttt{Nat}):

231\begin{SaveVerbatim}{bindef}

232

233data Binary : Nat -> Type where

234− bEnd : Binary O

234+ bEnd : Binary Z

235 bO : Binary n -> Binary (n + n)

236 bI : Binary n -> Binary (S (n + n))

237

@@ -263,7 +263,7 @@ provisional definition in the odd case:

263\begin{SaveVerbatim}{ntbdef}

264

265natToBin : (n:Nat) -> Binary n

266−natToBin O = bEnd

266+natToBin Z = bEnd

267natToBin (S k) with (parity k)

268 natToBin (S (j + j)) | even = bI (natToBin j)

269 natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))

tutorial/theorems.tex+46−46

@@ -42,11 +42,11 @@ to a successor:

43\begin{SaveVerbatim}{natdisjoint}

45−disjoint : (n : Nat) -> O = S n -> _|_

45+disjoint : (n : Nat) -> Z = S n -> _|_

46disjoint n p = replace {P = disjointTy} p ()

47 where

48 disjointTy : Nat -> Type

49− disjointTy O = ()

49+ disjointTy Z = ()

50 disjointTy (S k) = _|_

52\end{SaveVerbatim}

@@ -76,7 +76,7 @@ we want to prove the following theorem about the reduction behaviour of \texttt{

77\begin{SaveVerbatim}{plusred}

79−plusReduces : (n:Nat) -> plus O n = n

79+plusReduces : (n:Nat) -> plus Z n = n

81\end{SaveVerbatim}

82\useverb{plusred}

@@ -90,7 +90,7 @@ of interest.

91We won't go into details here, but the Curry-Howard

92correspondence~\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}

94by the definition of \texttt{plus}:

96\begin{SaveVerbatim}{plusredp}

@@ -107,9 +107,9 @@ on the first argument to \texttt{plus}, namely \texttt{n}.

107

108\begin{SaveVerbatim}{plusRedO}

109

110−plusReducesO : (n:Nat) -> n = plus n O

110+plusReducesZ : (n:Nat) -> n = plus n Z

111−plusReducesO O = refl

111+plusReducesZ Z = refl

112−plusReducesO (S k) = cong (plusReducesO k)

112+plusReducesZ (S k) = cong (plusReducesZ k)

113

114\end{SaveVerbatim}

115\useverb{plusRedO}

@@ -131,7 +131,7 @@ We can do the same for the reduction behaviour of plus on successors:

131\begin{SaveVerbatim}{plusRedS}

132

133plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)

134−plusReducesS O m = refl

134+plusReducesS Z m = refl

135plusReducesS (S k) m = cong (plusReducesS k m)

136

137\end{SaveVerbatim}

@@ -148,16 +148,16 @@ therefore provides an interactive proof mode.

148Instead of writing the proof in one go, we can use \Idris{}'s interactive

149proof mode. To do this, we write the general \emph{structure} of the proof,

150and 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

152\texttt{S}, with a recursive call in the \texttt{S} case giving the inductive

153hypothesis, and insert \emph{metavariables} for the rest of the definition:

154

155\begin{SaveVerbatim}{prOstruct}

156

157−plusReducesO' : (n:Nat) -> n = plus n O

157+plusReducesZ' : (n:Nat) -> n = plus n Z

158−plusReducesO' O = ?plusredO_O

158+plusReducesZ' Z = ?plusredZ_Z

159−plusReducesO' (S k) = let ih = plusReducesO' k in

159+plusReducesZ' (S k) = let ih = plusReducesZ' k in

160− ?plusredO_S

160+ ?plusredZ_S

161

162\end{SaveVerbatim}

163\useverb{prOstruct}

@@ -173,17 +173,17 @@ precisely, which functions exist but have no definitions), then the

173

174*theorems> :m

175Global metavariables:

176− [plusredO_S,plusredO_O]

176+ [plusredZ_S,plusredZ_Z]

177

178\end{SaveVerbatim}

179

180\begin{SaveVerbatim}{metatypes}

181

182−*theorems> :t plusredO_O

182+*theorems> :t plusredZ_Z

183−plusredO_O : O = plus O O

183+plusredZ_Z : Z = plus Z Z

184

185−*theorems> :t plusredO_S

185+*theorems> :t plusredZ_S

186−plusredO_S : (k : Nat) -> (k = plus k O) -> S k = S (plus k O)

186+plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = S (plus k Z)

187

188\end{SaveVerbatim}

189\useverb{showmetas}

@@ -196,10 +196,10 @@ the missing definitions.

196

197\begin{SaveVerbatim}{proveO}

198

199−*theorems> :p plusredO_O

199+*theorems> :p plusredZ_Z

200

201−---------------------------------- (plusredO_O) --------

201+---------------------------------- (plusredZ_Z) --------

202−{hole0} : O = plus O O

202+{hole0} : Z = plus Z Z

203

204\end{SaveVerbatim}

205\useverb{proveO}

@@ -213,24 +213,24 @@ we can normalise the goal with the \texttt{compute} tactic:

213

214\begin{SaveVerbatim}{compute}

215

216−-plusredO_O> compute

216+-plusredZ_Z> compute

217

218−---------------------------------- (plusredO_O) --------

218+---------------------------------- (plusredZ_Z) --------

219−{hole0} : O = O

219+{hole0} : Z = Z

220

221\end{SaveVerbatim}

222\useverb{compute}

223

224\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

226\texttt{refl}. To apply a function, such as \texttt{refl}, we use \texttt{refine}

227which introduces subgoals for each of the function's explicit arguments (\texttt{refl}

228has none):

229

230\begin{SaveVerbatim}{refrefl}

231

232−-plusredO_O> refine refl

232+-plusredZ_Z> refine refl

233−plusredO_O: no more goals

233+plusredZ_Z: no more goals

234

235\end{SaveVerbatim}

236\useverb{refrefl}

@@ -244,8 +244,8 @@ This also outputs a trace of the proof:

244

245\begin{SaveVerbatim}{prOprooftrace}

246

247−-plusredO_O> qed

247+-plusredZ_Z> qed

248−plusredO_O = proof {

248+plusredZ_Z = proof {

249 compute;

250 refine refl;

251}

@@ -257,7 +257,7 @@ plusredO_O = proof {

257

258*theorems> :m

259Global metavariables:

260− [plusredO_S]

260+ [plusredZ_S]

261

262\end{SaveVerbatim}

263\useverb{showmetasO}

@@ -269,10 +269,10 @@ Let us now prove the other required lemma, \texttt{plusredO\_S}:

269

270\begin{SaveVerbatim}{plusredOSprf}

271

272−*theorems> :p plusredO_S

272+*theorems> :p plusredZ_S

273

274−---------------------------------- (plusredO_S) --------

274+---------------------------------- (plusredZ_S) --------

275−{hole0} : (k : Nat) -> (k = plus k O) -> S k = S (plus k O)

275+{hole0} : (k : Nat) -> (k = plus k Z) -> S k = S (plus k Z)

276

277\end{SaveVerbatim}

278\useverb{plusredOSprf}

@@ -286,28 +286,28 @@ twice (or \texttt{intros}, which introduces all arguments as premisses). This gi

286\begin{SaveVerbatim}{prSintros}

287

288 k : Nat

289− ih : k = plus k O

289+ ih : k = plus k Z

290−---------------------------------- (plusredO_S) --------

290+---------------------------------- (plusredZ_S) --------

291−{hole2} : S k = S (plus k O)

291+{hole2} : S k = S (plus k Z)

292

293\end{SaveVerbatim}

294\useverb{prSintros}

295

296\noindent

297−We know, from the type of \texttt{ih}, that \texttt{k = plus k O}, so we would like to

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 O} in the goal with \texttt{k}. We can

298+use this knowledge to replace \texttt{plus k Z} in the goal with \texttt{k}. We can

299achieve this with the \texttt{rewrite} tactic:

300

301\begin{SaveVerbatim}{}

302

303−-plusredO_S> rewrite ih

303+-plusredZ_S> rewrite ih

304

305 k : Nat

306− ih : k = plus k O

306+ ih : k = plus k Z

307−---------------------------------- (plusredO_S) --------

307+---------------------------------- (plusredZ_S) --------

308{hole3} : S k = S k

309

310−-plusredO_S>

310+-plusredZ_S>

311

312\end{SaveVerbatim}

313\useverb{}

@@ -318,10 +318,10 @@ the goal using that proof. Here, it results in an equality which is trivially pr

318

319\begin{SaveVerbatim}{prOStrace}

320

321−-plusredO_S> trivial

321+-plusredZ_S> trivial

322−plusredO_S: no more goals

322+plusredZ_S: no more goals

323−-plusredO_S> qed

323+-plusredZ_S> qed

324−plusredO_S = proof {

324+plusredZ_S = proof {

325 intros;

326 rewrite ih;

327 trivial;

tutorial/typesfuns.tex+24−24

@@ -81,7 +81,7 @@ syntax. Natural numbers and lists, for example, can be declared as follows:

82\begin{SaveVerbatim}{natlist}

84−data Nat = O | S Nat -- Natural numbers

84+data Nat = Z | S Nat -- Natural numbers

85 -- (zero and successor)

86data List a = Nil | (::) a (List a) -- Polymorphic lists

@@ -90,7 +90,7 @@ data List a = Nil | (::) a (List a) -- Polymorphic lists

91\noindent

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

94the successor of another natural number (\texttt{S k}).

95Lists can either be empty (\texttt{Nil})

96or 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:

132

133-- Unary addition

134plus : Nat -> Nat -> Nat

135−plus O y = y

135+plus Z y = y

136plus (S k) y = S (plus k y)

137

138-- Unary multiplication

139mult : Nat -> Nat -> Nat

140−mult O y = O

140+mult Z y = Z

141mult (S k) y = plus y (mult k y)

142

143\end{SaveVerbatim}

@@ -148,7 +148,7 @@ The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded

148for use by \texttt{Nat}, and are implemented

149using the above functions. Unlike Haskell, there is no restriction on whether

150types 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},

152\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are

153all part of the same namespace.

154

@@ -156,10 +156,10 @@ We can test these functions at the \Idris{} prompt:

156

157\begin{SaveVerbatim}{fntest}

158

159−Idris> plus (S (S O)) (S (S O))

159+Idris> plus (S (S Z)) (S (S Z))

160−S (S (S (S O))) : Nat

160+S (S (S (S Z))) : Nat

161−Idris> mult (S (S (S O))) (plus (S (S O)) (S (S O)))

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 O))))))))))) : Nat

162+S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) : Nat

163

164\end{SaveVerbatim}

165\useverb{fntest}

@@ -171,9 +171,9 @@ meaning that we can also test the functions as follows:

171\begin{SaveVerbatim}{fntest}

172

173Idris> plus 2 2

174−S (S (S (S O))) : Nat

174+S (S (S (S Z))) : Nat

175Idris> 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

177

178\end{SaveVerbatim}

179\useverb{fntest}

@@ -252,13 +252,13 @@ So, for example, the following definitions are legal:

252\begin{SaveVerbatim}{whereinfer}

253

254even : Nat -> Bool

255−even O = True

255+even Z = True

256even (S k) = odd k where

257− odd O = False

257+ odd Z = False

258 odd (S k) = even k

259

260test : List Nat

261−test = [c (S 1), c O, d (S O)]

261+test = [c (S 1), c Z, d (S Z)]

262 where c x = 42 + x

263 d y = c (y + 1 + z y)

264 where z w = y + w

@@ -278,7 +278,7 @@ we declare vectors as follows:

278\begin{SaveVerbatim}{vect}

279

280data Vect : Type -> Nat -> Type where

281− Nil : Vect a O

281+ Nil : Vect a Z

282 (::) : a -> Vect a k -> Vect a (S k)

283

284\end{SaveVerbatim}

@@ -366,12 +366,12 @@ data Fin : Nat -> Type where

366\useverb{findecl}

367

368\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;

370\texttt{fS n} is the

371\texttt{n+1}th element of a finite set with \texttt{S k} elements.

372\tTC{Fin} is indexed by a \tTC{Nat}, which

373represents 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}.

375

376A useful application of the \tTC{Fin} family is to represent bounded

377natural 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

397is no larger than the length of the vector.

398

399Note 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

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{O}. As a result, attempting to

401+\texttt{Fin n}, then \texttt{n} can not be \tDC{Z}. As a result, attempting to

402look 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}.

404

405\subsubsection{Implicit Arguments}

406

@@ -520,11 +520,11 @@ data types and functions to be defined simultaneously:

520

521mutual

522 even : Nat -> Bool

523− even O = True

523+ even Z = True

524 even (S k) = odd k

525

526 odd : Nat -> Bool

527− odd O = False

527+ odd Z = False

528 odd (S k) = even k

529

530\end{SaveVerbatim}

@@ -663,7 +663,7 @@ We have already seen the \texttt{List} and \texttt{Vect} data types:

663data List a = Nil | (::) a (List a)

664

665data Vect : Type -> Nat -> Type where

666− Nil : Vect a O

666+ Nil : Vect a Z

667 (::) : a -> Vect a k -> Vect a (S k)

668

669\end{SaveVerbatim}

@@ -787,7 +787,7 @@ bounds error:

787

788list_lookup : Nat -> List a -> Maybe a

789list_lookup _ Nil = Nothing

790−list_lookup O (x :: xs) = Just x

790+list_lookup Z (x :: xs) = Just x

791list_lookup (S k) (x :: xs) = list_lookup k xs

792

793\end{SaveVerbatim}

tutorial/views.tex+2−2

@@ -10,7 +10,7 @@ determined by whether the vector was empty or not:

10\begin{SaveVerbatim}{appdep}

12(++) : Vect a n -> Vect a m -> Vect a (n + m)

13−(++) {n=O} [] ys = ys

13+(++) {n=Z} [] ys = ys

14(++) {n=S k} (x :: xs) ys = x :: xs ++ ys

16\end{SaveVerbatim}

@@ -83,7 +83,7 @@ to write a function which converts a natural number to a list of binary digits

83\begin{SaveVerbatim}{natToBin}

85natToBin : Nat -> List Bool

86−natToBin O = Nil

86+natToBin Z = Nil

87natToBin k with (parity k)

88 natToBin (j + j) | even = False :: natToBin j

89 natToBin (S (j + j)) | odd = True :: natToBin j