diff --git a/effects/Effect/Memory.idr b/effects/Effect/Memory.idr index 281303cae..6d722a19c 100644 --- a/effects/Effect/Memory.idr +++ b/effects/Effect/Memory.idr @@ -63,7 +63,7 @@ do_memmove dest src dest_offset src_offset size private do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect Bits8 size) -do_peek _ _ O = return (Prelude.Vect.Nil) +do_peek _ _ Z = return (Prelude.Vect.Nil) do_peek ptr offset (S n) = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FByte) ptr (fromInteger $ cast offset) bs <- do_peek ptr (S offset) n diff --git a/effects/Effects.idr b/effects/Effects.idr index 45ff4b8e9..3ddbf9d25 100644 --- a/effects/Effects.idr +++ b/effects/Effects.idr @@ -63,13 +63,13 @@ rebuildEnv (x :: xs) SubNil [] = x :: xs -- some proof automation findEffElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic -- Nat is maximum search depth -findEffElem O ctxt goal = Refine "Here" `Seq` Solve +findEffElem Z ctxt goal = Refine "Here" `Seq` Solve findEffElem (S n) ctxt goal = GoalType "EffElem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findEffElem n ctxt goal))) findSubList : Nat -> List (TTName, Binder TT) -> TT -> Tactic -findSubList O ctxt goal = Refine "SubNil" `Seq` Solve +findSubList Z ctxt goal = Refine "SubNil" `Seq` Solve findSubList (S n) ctxt goal = GoalType "SubList" (Try (Refine "subListId" `Seq` Solve) diff --git a/lib/Data/Bits.idr b/lib/Data/Bits.idr index 5e3646489..ed625f46b 100644 --- a/lib/Data/Bits.idr +++ b/lib/Data/Bits.idr @@ -4,11 +4,11 @@ module Data.Bits divCeil : Nat -> Nat -> Nat divCeil x y = case x `mod` y of - O => x `div` y + Z => x `div` y S _ => S (x `div` y) nextPow2 : Nat -> Nat -nextPow2 O = O +nextPow2 Z = Z nextPow2 x = if x == (2 `power` l2x) then l2x else S l2x @@ -19,9 +19,9 @@ nextBytes : Nat -> Nat nextBytes bits = (nextPow2 (bits `divCeil` 8)) machineTy : Nat -> Type -machineTy O = Bits8 -machineTy (S O) = Bits16 -machineTy (S (S O)) = Bits32 +machineTy Z = Bits8 +machineTy (S Z) = Bits16 +machineTy (S (S Z)) = Bits32 machineTy (S (S (S _))) = Bits64 bitsUsed : Nat -> Nat @@ -29,19 +29,19 @@ bitsUsed n = 8 * (2 `power` n) %assert_total natToBits' : machineTy n -> Nat -> machineTy n -natToBits' a O = a +natToBits' a Z = a natToBits' {n=n} a x with n -- it seems I have to manually recover the value of n here, instead of being able to reference it - natToBits' a (S x') | O = natToBits' {n=0} (prim__addB8 a (prim__truncInt_B8 1)) x' - natToBits' a (S x') | S O = natToBits' {n=1} (prim__addB16 a (prim__truncInt_B16 1)) x' - natToBits' a (S x') | S (S O) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x' + natToBits' a (S x') | Z = natToBits' {n=0} (prim__addB8 a (prim__truncInt_B8 1)) x' + natToBits' a (S x') | S Z = natToBits' {n=1} (prim__addB16 a (prim__truncInt_B16 1)) x' + natToBits' a (S x') | S (S Z) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x' natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x' natToBits : Nat -> machineTy n natToBits {n=n} x with n - | O = natToBits' {n=0} (prim__truncInt_B8 0) x - | S O = natToBits' {n=1} (prim__truncInt_B16 0) x - | S (S O) = natToBits' {n=2} (prim__truncInt_B32 0) x + | Z = natToBits' {n=0} (prim__truncInt_B8 0) x + | S Z = natToBits' {n=1} (prim__truncInt_B16 0) x + | S (S Z) = natToBits' {n=2} (prim__truncInt_B32 0) x | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x getPad : Nat -> machineTy n @@ -94,9 +94,9 @@ pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) shiftLeft' {n=n} x c with (nextBytes n) - | O = pad8' n prim__shlB8 x c - | S O = pad16' n prim__shlB16 x c - | S (S O) = pad32' n prim__shlB32 x c + | Z = pad8' n prim__shlB8 x c + | S Z = pad16' n prim__shlB16 x c + | S (S Z) = pad32' n prim__shlB32 x c | S (S (S _)) = pad64' n prim__shlB64 x c public @@ -105,9 +105,9 @@ shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y) shiftRightLogical' : machineTy n -> machineTy n -> machineTy n shiftRightLogical' {n=n} x c with n - | O = prim__lshrB8 x c - | S O = prim__lshrB16 x c - | S (S O) = prim__lshrB32 x c + | Z = prim__lshrB8 x c + | S Z = prim__lshrB16 x c + | S (S Z) = prim__lshrB32 x c | S (S (S _)) = prim__lshrB64 x c public @@ -117,9 +117,9 @@ shiftRightLogical {n} (MkBits x) (MkBits y) shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) shiftRightArithmetic' {n=n} x c with (nextBytes n) - | O = pad8' n prim__ashrB8 x c - | S O = pad16' n prim__ashrB16 x c - | S (S O) = pad32' n prim__ashrB32 x c + | Z = pad8' n prim__ashrB8 x c + | S Z = pad16' n prim__ashrB16 x c + | S (S Z) = pad32' n prim__ashrB32 x c | S (S (S _)) = pad64' n prim__ashrB64 x c public @@ -128,9 +128,9 @@ shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y) and' : machineTy n -> machineTy n -> machineTy n and' {n=n} x y with n - | O = prim__andB8 x y - | S O = prim__andB16 x y - | S (S O) = prim__andB32 x y + | Z = prim__andB8 x y + | S Z = prim__andB16 x y + | S (S Z) = prim__andB32 x y | S (S (S _)) = prim__andB64 x y public @@ -139,9 +139,9 @@ and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y) or' : machineTy n -> machineTy n -> machineTy n or' {n=n} x y with n - | O = prim__orB8 x y - | S O = prim__orB16 x y - | S (S O) = prim__orB32 x y + | Z = prim__orB8 x y + | S Z = prim__orB16 x y + | S (S Z) = prim__orB32 x y | S (S (S _)) = prim__orB64 x y public @@ -150,9 +150,9 @@ or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y) xor' : machineTy n -> machineTy n -> machineTy n xor' {n=n} x y with n - | O = prim__xorB8 x y - | S O = prim__xorB16 x y - | S (S O) = prim__xorB32 x y + | Z = prim__xorB8 x y + | S Z = prim__xorB16 x y + | S (S Z) = prim__xorB32 x y | S (S (S _)) = prim__xorB64 x y public @@ -161,9 +161,9 @@ xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y) plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) plus' {n=n} x y with (nextBytes n) - | O = pad8 n prim__addB8 x y - | S O = pad16 n prim__addB16 x y - | S (S O) = pad32 n prim__addB32 x y + | Z = pad8 n prim__addB8 x y + | S Z = pad16 n prim__addB16 x y + | S (S Z) = pad32 n prim__addB32 x y | S (S (S _)) = pad64 n prim__addB64 x y public @@ -172,9 +172,9 @@ plus (MkBits x) (MkBits y) = MkBits (plus' x y) minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) minus' {n=n} x y with (nextBytes n) - | O = pad8 n prim__subB8 x y - | S O = pad16 n prim__subB16 x y - | S (S O) = pad32 n prim__subB32 x y + | Z = pad8 n prim__subB8 x y + | S Z = pad16 n prim__subB16 x y + | S (S Z) = pad32 n prim__subB32 x y | S (S (S _)) = pad64 n prim__subB64 x y public @@ -183,9 +183,9 @@ minus (MkBits x) (MkBits y) = MkBits (minus' x y) times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) times' {n=n} x y with (nextBytes n) - | O = pad8 n prim__mulB8 x y - | S O = pad16 n prim__mulB16 x y - | S (S O) = pad32 n prim__mulB32 x y + | Z = pad8 n prim__mulB8 x y + | S Z = pad16 n prim__mulB16 x y + | S (S Z) = pad32 n prim__mulB32 x y | S (S (S _)) = pad64 n prim__mulB64 x y public @@ -195,9 +195,9 @@ times (MkBits x) (MkBits y) = MkBits (times' x y) partial sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) sdiv' {n=n} x y with (nextBytes n) - | O = prim__sdivB8 x y - | S O = prim__sdivB16 x y - | S (S O) = prim__sdivB32 x y + | Z = prim__sdivB8 x y + | S Z = prim__sdivB16 x y + | S (S Z) = prim__sdivB32 x y | S (S (S _)) = prim__sdivB64 x y public partial @@ -207,9 +207,9 @@ sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y) partial udiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) udiv' {n=n} x y with (nextBytes n) - | O = prim__udivB8 x y - | S O = prim__udivB16 x y - | S (S O) = prim__udivB32 x y + | Z = prim__udivB8 x y + | S Z = prim__udivB16 x y + | S (S Z) = prim__udivB32 x y | S (S (S _)) = prim__udivB64 x y public partial @@ -219,9 +219,9 @@ udiv (MkBits x) (MkBits y) = MkBits (udiv' x y) partial srem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) srem' {n=n} x y with (nextBytes n) - | O = prim__sremB8 x y - | S O = prim__sremB16 x y - | S (S O) = prim__sremB32 x y + | Z = prim__sremB8 x y + | S Z = prim__sremB16 x y + | S (S Z) = prim__sremB32 x y | S (S (S _)) = prim__sremB64 x y public partial @@ -231,9 +231,9 @@ srem (MkBits x) (MkBits y) = MkBits (srem' x y) partial urem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) urem' {n=n} x y with (nextBytes n) - | O = prim__uremB8 x y - | S O = prim__uremB16 x y - | S (S O) = prim__uremB32 x y + | Z = prim__uremB8 x y + | S Z = prim__uremB16 x y + | S (S Z) = prim__uremB32 x y | S (S (S _)) = prim__uremB64 x y public partial @@ -243,37 +243,37 @@ urem (MkBits x) (MkBits y) = MkBits (urem' x y) -- TODO: Proofy comparisons via postulates lt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int lt {n=n} x y with (nextBytes n) - | O = prim__ltB8 x y - | S O = prim__ltB16 x y - | S (S O) = prim__ltB32 x y + | Z = prim__ltB8 x y + | S Z = prim__ltB16 x y + | S (S Z) = prim__ltB32 x y | S (S (S _)) = prim__ltB64 x y lte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int lte {n=n} x y with (nextBytes n) - | O = prim__lteB8 x y - | S O = prim__lteB16 x y - | S (S O) = prim__lteB32 x y + | Z = prim__lteB8 x y + | S Z = prim__lteB16 x y + | S (S Z) = prim__lteB32 x y | S (S (S _)) = prim__lteB64 x y eq : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int eq {n=n} x y with (nextBytes n) - | O = prim__eqB8 x y - | S O = prim__eqB16 x y - | S (S O) = prim__eqB32 x y + | Z = prim__eqB8 x y + | S Z = prim__eqB16 x y + | S (S Z) = prim__eqB32 x y | S (S (S _)) = prim__eqB64 x y gte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int gte {n=n} x y with (nextBytes n) - | O = prim__gteB8 x y - | S O = prim__gteB16 x y - | S (S O) = prim__gteB32 x y + | Z = prim__gteB8 x y + | S Z = prim__gteB16 x y + | S (S Z) = prim__gteB32 x y | S (S (S _)) = prim__gteB64 x y gt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int gt {n=n} x y with (nextBytes n) - | O = prim__gtB8 x y - | S O = prim__gtB16 x y - | S (S O) = prim__gtB32 x y + | Z = prim__gtB8 x y + | S Z = prim__gtB16 x y + | S (S Z) = prim__gtB32 x y | S (S (S _)) = prim__gtB64 x y instance Eq (Bits n) where @@ -293,11 +293,11 @@ instance Ord (Bits n) where complement' : machineTy (nextBytes n) -> machineTy (nextBytes n) complement' {n=n} x with (nextBytes n) - | O = let pad = getPad {n=0} n in + | Z = let pad = getPad {n=0} n in prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad - | S O = let pad = getPad {n=1} n in + | S Z = let pad = getPad {n=1} n in prim__complB16 (x `prim__shlB16` pad) `prim__lshrB16` pad - | S (S O) = let pad = getPad {n=2} n in + | S (S Z) = let pad = getPad {n=2} n in prim__complB32 (x `prim__shlB32` pad) `prim__lshrB32` pad | S (S (S _)) = let pad = getPad {n=3} n in prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad @@ -309,15 +309,15 @@ complement (MkBits x) = MkBits (complement' x) -- TODO: Prove zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m)) zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m)) - | (O, O) = believe_me x - | (O, S O) = believe_me (prim__zextB8_B16 (believe_me x)) - | (O, S (S O)) = believe_me (prim__zextB8_B32 (believe_me x)) - | (O, S (S (S _))) = believe_me (prim__zextB8_B64 (believe_me x)) - | (S O, S O) = believe_me x - | (S O, S (S O)) = believe_me (prim__zextB16_B32 (believe_me x)) - | (S O, S (S (S _))) = believe_me (prim__zextB16_B64 (believe_me x)) - | (S (S O), S (S O)) = believe_me x - | (S (S O), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x)) + | (Z, Z) = believe_me x + | (Z, S Z) = believe_me (prim__zextB8_B16 (believe_me x)) + | (Z, S (S Z)) = believe_me (prim__zextB8_B32 (believe_me x)) + | (Z, S (S (S _))) = believe_me (prim__zextB8_B64 (believe_me x)) + | (S Z, S Z) = believe_me x + | (S Z, S (S Z)) = believe_me (prim__zextB16_B32 (believe_me x)) + | (S Z, S (S (S _))) = believe_me (prim__zextB16_B64 (believe_me x)) + | (S (S Z), S (S Z)) = believe_me x + | (S (S Z), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x)) | (S (S (S _)), S (S (S _))) = believe_me x public @@ -327,11 +327,11 @@ zeroExtend (MkBits x) = MkBits (zext' x) %assert_total intToBits' : Integer -> machineTy (nextBytes n) intToBits' {n=n} x with (nextBytes n) - | O = let pad = getPad {n=0} n in + | Z = let pad = getPad {n=0} n in prim__lshrB8 (prim__shlB8 (prim__truncBigInt_B8 x) pad) pad - | S O = let pad = getPad {n=1} n in + | S Z = let pad = getPad {n=1} n in prim__lshrB16 (prim__shlB16 (prim__truncBigInt_B16 x) pad) pad - | S (S O) = let pad = getPad {n=2} n in + | S (S Z) = let pad = getPad {n=2} n in prim__lshrB32 (prim__shlB32 (prim__truncBigInt_B32 x) pad) pad | S (S (S _)) = let pad = getPad {n=3} n in prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad @@ -345,9 +345,9 @@ instance Cast Integer (Bits n) where bitsToInt' : machineTy (nextBytes n) -> Integer bitsToInt' {n=n} x with (nextBytes n) - | O = prim__zextB8_BigInt x - | S O = prim__zextB16_BigInt x - | S (S O) = prim__zextB32_BigInt x + | Z = prim__zextB8_BigInt x + | S Z = prim__zextB16_BigInt x + | S (S Z) = prim__zextB32_BigInt x | S (S (S _)) = prim__zextB64_BigInt x public @@ -364,28 +364,28 @@ bitsToInt (MkBits x) = bitsToInt' x -- TODO: Prove sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m)) sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m)) - | (O, O) = let pad = getPad {n=0} n in + | (Z, Z) = let pad = getPad {n=0} n in believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad) - | (O, S O) = let pad = getPad {n=0} n in + | (Z, S Z) = let pad = getPad {n=0} n in believe_me (prim__ashrB16 (prim__sextB8_B16 (prim__shlB8 (believe_me x) pad)) (prim__zextB8_B16 pad)) - | (O, S (S O)) = let pad = getPad {n=0} n in + | (Z, S (S Z)) = let pad = getPad {n=0} n in believe_me (prim__ashrB32 (prim__sextB8_B32 (prim__shlB8 (believe_me x) pad)) (prim__zextB8_B32 pad)) - | (O, S (S (S _))) = let pad = getPad {n=0} n in + | (Z, S (S (S _))) = let pad = getPad {n=0} n in believe_me (prim__ashrB64 (prim__sextB8_B64 (prim__shlB8 (believe_me x) pad)) (prim__zextB8_B64 pad)) - | (S O, S O) = let pad = getPad {n=1} n in + | (S Z, S Z) = let pad = getPad {n=1} n in believe_me (prim__ashrB16 (prim__shlB16 (believe_me x) pad) pad) - | (S O, S (S O)) = let pad = getPad {n=1} n in + | (S Z, S (S Z)) = let pad = getPad {n=1} n in believe_me (prim__ashrB32 (prim__sextB16_B32 (prim__shlB16 (believe_me x) pad)) (prim__zextB16_B32 pad)) - | (S O, S (S (S _))) = let pad = getPad {n=1} n in + | (S Z, S (S (S _))) = let pad = getPad {n=1} n in believe_me (prim__ashrB64 (prim__sextB16_B64 (prim__shlB16 (believe_me x) pad)) (prim__zextB16_B64 pad)) - | (S (S O), S (S O)) = let pad = getPad {n=2} n in + | (S (S Z), S (S Z)) = let pad = getPad {n=2} n in believe_me (prim__ashrB32 (prim__shlB32 (believe_me x) pad) pad) - | (S (S O), S (S (S _))) = let pad = getPad {n=2} n in + | (S (S Z), S (S (S _))) = let pad = getPad {n=2} n in believe_me (prim__ashrB64 (prim__sextB32_B64 (prim__shlB32 (believe_me x) pad)) (prim__zextB32_B64 pad)) | (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)) -- TODO: Prove trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n) trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m)) - | (O, O) = believe_me x - | (O, S O) = believe_me (prim__truncB16_B8 (believe_me x)) - | (O, S (S O)) = believe_me (prim__truncB32_B8 (believe_me x)) - | (O, S (S (S _))) = believe_me (prim__truncB64_B8 (believe_me x)) - | (S O, S O) = believe_me x - | (S O, S (S O)) = believe_me (prim__truncB32_B16 (believe_me x)) - | (S O, S (S (S _))) = believe_me (prim__truncB64_B16 (believe_me x)) - | (S (S O), S (S O)) = believe_me x - | (S (S O), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x)) + | (Z, Z) = believe_me x + | (Z, S Z) = believe_me (prim__truncB16_B8 (believe_me x)) + | (Z, S (S Z)) = believe_me (prim__truncB32_B8 (believe_me x)) + | (Z, S (S (S _))) = believe_me (prim__truncB64_B8 (believe_me x)) + | (S Z, S Z) = believe_me x + | (S Z, S (S Z)) = believe_me (prim__truncB32_B16 (believe_me x)) + | (S Z, S (S (S _))) = believe_me (prim__truncB64_B16 (believe_me x)) + | (S (S Z), S (S Z)) = believe_me x + | (S (S Z), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x)) | (S (S (S _)), S (S (S _))) = believe_me x --public diff --git a/lib/Data/BoundedList.idr b/lib/Data/BoundedList.idr index ef1ccdf35..91d4bc270 100644 --- a/lib/Data/BoundedList.idr +++ b/lib/Data/BoundedList.idr @@ -34,7 +34,7 @@ weaken (x :: xs) = x :: weaken xs take : (n : Nat) -> List a -> BoundedList a n take _ [] = [] -take O _ = [] +take Z _ = [] take (S n') (x :: xs) = x :: take n' xs toList : BoundedList a n -> List a @@ -50,7 +50,7 @@ fromList (x :: xs) = x :: fromList xs -------------------------------------------------------------------------------- replicate : (n : Nat) -> a -> BoundedList a n -replicate O _ = [] +replicate Z _ = [] replicate (S n) x = x :: replicate n x -------------------------------------------------------------------------------- @@ -79,7 +79,7 @@ map f (x :: xs) = f x :: map f xs %assert_total -- not sure why this isn't accepted - clearly decreasing on n pad : (xs : BoundedList a n) -> (padding : a) -> BoundedList a n -pad {n=O} [] _ = [] +pad {n=Z} [] _ = [] pad {n=S n'} [] padding = padding :: (pad {n=n'} [] padding) pad {n=S n'} (x :: xs) padding = x :: pad {n=n'} xs padding diff --git a/lib/Data/HVect.idr b/lib/Data/HVect.idr index faf2267cd..6e6eb2247 100644 --- a/lib/Data/HVect.idr +++ b/lib/Data/HVect.idr @@ -40,7 +40,7 @@ using (k : Nat, ts : Vect Type k) class Shows (k : Nat) (ts : Vect Type k) where shows : HVect ts -> Vect String k - instance Shows O [] where + instance Shows Z [] where shows [] = [] instance (Show t, Shows k ts) => Shows (S k) (t::ts) where diff --git a/lib/Data/SortedMap.idr b/lib/Data/SortedMap.idr index b348908db..13f25335b 100644 --- a/lib/Data/SortedMap.idr +++ b/lib/Data/SortedMap.idr @@ -3,7 +3,7 @@ module Data.SortedMap -- TODO: write merge and split data Tree : Nat -> Type -> Type -> Type where - Leaf : k -> v -> Tree O k v + Leaf : k -> v -> Tree Z k v Branch2 : Tree n k v -> k -> Tree n k v -> Tree (S n) k v 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 = Right (a, b, c) => Right (Branch2 a b c) delType : Nat -> Type -> Type -> Type -delType O k v = () +delType Z k v = () delType (S n) k v = Tree n k v treeDelete : 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) = Right () else Left (Leaf k' v) -treeDelete {n=S O} k (Branch2 t1 k' t2) = +treeDelete {n=S Z} k (Branch2 t1 k' t2) = if k <= k' then case treeDelete k t1 of Left t1' => Left (Branch2 t1' k' t2) @@ -141,7 +141,7 @@ treeDelete {n=S O} k (Branch2 t1 k' t2) = case treeDelete k t2 of Left t2' => Left (Branch2 t1 k' t2') Right () => Right t1 -treeDelete {n=S O} k (Branch3 t1 k1 t2 k2 t3) = +treeDelete {n=S Z} k (Branch3 t1 k1 t2 k2 t3) = if k <= k1 then case treeDelete k t1 of Left t1' => Left (Branch3 t1' k1 t2 k2 t3) @@ -201,7 +201,7 @@ lookup _ Empty = Nothing lookup k (M _ t) = treeLookup k t insert : Ord k => k -> v -> SortedMap k v -> SortedMap k v -insert k v Empty = M O (Leaf k v) +insert k v Empty = M Z (Leaf k v) insert k v (M _ t) = case treeInsert k v t of Left t' => (M _ t') @@ -209,7 +209,7 @@ insert k v (M _ t) = delete : Ord k => k -> SortedMap k v -> SortedMap k v delete _ Empty = Empty -delete k (M O t) = +delete k (M Z t) = case treeDelete k t of Left t' => (M _ t') Right () => Empty diff --git a/lib/Data/Vect.idr b/lib/Data/Vect.idr index fec977daa..f025aeac2 100644 --- a/lib/Data/Vect.idr +++ b/lib/Data/Vect.idr @@ -14,7 +14,7 @@ data Elem : a -> Vect a k -> Type where There : {xs : Vect a k} -> Elem x xs -> Elem x (y::xs) findElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic -findElem O ctxt goal = Refine "Here" `Seq` Solve +findElem Z ctxt goal = Refine "Here" `Seq` Solve findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal))) replaceElem : (xs : Vect t k) -> Elem x xs -> (y : t) -> (ys : Vect t k ** Elem y ys) diff --git a/lib/Data/ZZ.idr b/lib/Data/ZZ.idr index a33b0e783..aa6aaee88 100644 --- a/lib/Data/ZZ.idr +++ b/lib/Data/ZZ.idr @@ -24,17 +24,17 @@ instance Show ZZ where show (NegS n) = "-" ++ show (S n) negZ : ZZ -> ZZ -negZ (Pos O) = Pos O +negZ (Pos Z) = Pos Z negZ (Pos (S n)) = NegS n negZ (NegS n) = Pos (S n) negNat : Nat -> ZZ -negNat O = Pos O +negNat Z = Pos Z negNat (S n) = NegS n minusNatZ : Nat -> Nat -> ZZ -minusNatZ n O = Pos n -minusNatZ O (S m) = NegS m +minusNatZ n Z = Pos n +minusNatZ Z (S m) = NegS m minusNatZ (S n) (S m) = minusNatZ n m plusZ : ZZ -> ZZ -> ZZ @@ -101,9 +101,9 @@ natMultZMult : (n : Nat) -> (m : Nat) -> (x : Nat) natMultZMult n m x h = cong h doubleNegElim : (z : ZZ) -> negZ (negZ z) = z -doubleNegElim (Pos O) = refl +doubleNegElim (Pos Z) = refl doubleNegElim (Pos (S n)) = refl -doubleNegElim (NegS O) = refl +doubleNegElim (NegS Z) = refl doubleNegElim (NegS (S n)) = refl -- Injectivity diff --git a/lib/Decidable/Equality.idr b/lib/Decidable/Equality.idr index a7968dfcf..3fce338c1 100644 --- a/lib/Decidable/Equality.idr +++ b/lib/Decidable/Equality.idr @@ -41,13 +41,13 @@ instance DecEq Bool where -- Nat -------------------------------------------------------------------------------- -total OnotS : O = S n -> _|_ +total OnotS : Z = S n -> _|_ OnotS refl impossible instance DecEq Nat where - decEq O O = Yes refl - decEq O (S _) = No OnotS - decEq (S _) O = No (negEqSym OnotS) + decEq Z Z = Yes refl + decEq Z (S _) = No OnotS + decEq (S _) Z = No (negEqSym OnotS) decEq (S n) (S m) with (decEq n m) | Yes p = Yes $ cong p | No p = No $ \h : (S n = S m) => p $ succInjective n m h diff --git a/lib/Decidable/Order.idr b/lib/Decidable/Order.idr index 84c6a2153..a4f48e539 100644 --- a/lib/Decidable/Order.idr +++ b/lib/Decidable/Order.idr @@ -55,7 +55,7 @@ NatLTEIsAntisymmetric n m (nLTESm _) (nLTESm _) impossible instance Poset Nat NatLTE where antisymmetric = NatLTEIsAntisymmetric -total zeroNeverGreater : {n : Nat} -> NatLTE (S n) O -> _|_ +total zeroNeverGreater : {n : Nat} -> NatLTE (S n) Z -> _|_ zeroNeverGreater {n} (nLTESm _) impossible zeroNeverGreater {n} nEqn impossible @@ -66,8 +66,8 @@ nGTSm {n} {m} disprf (nEqn) impossible total decideNatLTE : (n : Nat) -> (m : Nat) -> Dec (NatLTE n m) -decideNatLTE O O = Yes nEqn -decideNatLTE (S x) O = No zeroNeverGreater +decideNatLTE Z Z = Yes nEqn +decideNatLTE (S x) Z = No zeroNeverGreater decideNatLTE x (S y) with (decEq x (S y)) | Yes eq = rewrite eq in Yes nEqn | No _ with (decideNatLTE x y) diff --git a/lib/Prelude.idr b/lib/Prelude.idr index 2953dd5d7..6104522bc 100644 --- a/lib/Prelude.idr +++ b/lib/Prelude.idr @@ -251,7 +251,7 @@ instance Monad List where %lib C "m" pow : (Num a) => a -> Nat -> a -pow x O = 1 +pow x Z = 1 pow x (S n) = x * (pow x n) exp : Float -> Float diff --git a/lib/Prelude/Fin.idr b/lib/Prelude/Fin.idr index e3a91ec08..3e528927e 100644 --- a/lib/Prelude/Fin.idr +++ b/lib/Prelude/Fin.idr @@ -17,7 +17,7 @@ finToNat fO a = a finToNat (fS x) a = finToNat x (S a) instance Cast (Fin n) Nat where - cast x = finToNat x O + cast x = finToNat x Z finToInt : Fin n -> Integer -> Integer finToInt fO a = a @@ -38,7 +38,7 @@ strengthen {n = S k} (fS i) with (strengthen i) strengthen f = Left f last : Fin (S n) -last {n=O} = fO +last {n=Z} = fO last {n=S _} = fS last total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f' @@ -48,7 +48,7 @@ fSinjective refl = refl -- Construct a Fin from an integer literal which must fit in the given Fin natToFin : Nat -> (n : Nat) -> Maybe (Fin n) -natToFin O (S j) = Just fO +natToFin Z (S j) = Just fO natToFin (S k) (S j) with (natToFin k j) | Just k' = Just (fS k') | Nothing = Nothing diff --git a/lib/Prelude/Heap.idr b/lib/Prelude/Heap.idr index edad72bee..b449372e4 100644 --- a/lib/Prelude/Heap.idr +++ b/lib/Prelude/Heap.idr @@ -27,7 +27,7 @@ isEmpty Empty = True isEmpty _ = False total size : MaxiphobicHeap a -> Nat -size Empty = O +size Empty = Z size (Node s l e r) = s isValidHeap : Ord a => MaxiphobicHeap a -> Bool @@ -148,7 +148,7 @@ absurdBoolDischarge p = replace {P = disjointTy} p () disjointTy False = () disjointTy True = _|_ -total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = O +total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z isEmptySizeZero Empty p = refl isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd diff --git a/lib/Prelude/List.idr b/lib/Prelude/List.idr index 4d386ba8f..69fbb750c 100644 --- a/lib/Prelude/List.idr +++ b/lib/Prelude/List.idr @@ -85,12 +85,12 @@ init' (x::xs) = -------------------------------------------------------------------------------- take : Nat -> List a -> List a -take O xs = [] +take Z xs = [] take (S n) [] = [] take (S n) (x::xs) = x :: take n xs drop : Nat -> List a -> List a -drop O xs = xs +drop Z xs = xs drop (S n) [] = [] drop (S n) (x::xs) = drop n xs @@ -127,7 +127,7 @@ repeat : a -> List a repeat x = x :: lazy (repeat x) replicate : Nat -> a -> List a -replicate O x = [] +replicate Z x = [] replicate (S n) x = x :: replicate n x -------------------------------------------------------------------------------- @@ -325,7 +325,7 @@ find p (x::xs) = find p xs findIndex : (a -> Bool) -> List a -> Maybe Nat -findIndex = findIndex' O +findIndex = findIndex' Z where -- findIndex' : Nat -> (a -> Bool) -> List a -> Maybe Nat findIndex' cnt p [] = Nothing @@ -336,7 +336,7 @@ findIndex = findIndex' O findIndex' (S cnt) p xs findIndices : (a -> Bool) -> List a -> List Nat -findIndices = findIndices' O +findIndices = findIndices' Z where -- findIndices' : Nat -> (a -> Bool) -> List a -> List Nat findIndices' cnt p [] = [] diff --git a/lib/Prelude/Nat.idr b/lib/Prelude/Nat.idr index b30814705..17d767ab1 100644 --- a/lib/Prelude/Nat.idr +++ b/lib/Prelude/Nat.idr @@ -9,7 +9,7 @@ import Prelude.Cast %default total data Nat - = O + = Z | S Nat -------------------------------------------------------------------------------- @@ -17,11 +17,11 @@ data Nat -------------------------------------------------------------------------------- total isZero : Nat -> Bool -isZero O = True +isZero Z = True isZero (S n) = False total isSucc : Nat -> Bool -isSucc O = False +isSucc Z = False isSucc (S n) = True -------------------------------------------------------------------------------- @@ -29,27 +29,27 @@ isSucc (S n) = True -------------------------------------------------------------------------------- total plus : Nat -> Nat -> Nat -plus O right = right +plus Z right = right plus (S left) right = S (plus left right) total mult : Nat -> Nat -> Nat -mult O right = O +mult Z right = Z mult (S left) right = plus right $ mult left right total minus : Nat -> Nat -> Nat -minus O right = O -minus left O = left +minus Z right = Z +minus left Z = left minus (S left) (S right) = minus left right total power : Nat -> Nat -> Nat -power base O = S O +power base Z = S Z power base (S exp) = mult base $ power base exp hyper : Nat -> Nat -> Nat -> Nat -hyper O a b = S b -hyper (S O) a O = a -hyper (S(S O)) a O = O -hyper n a O = S O +hyper Z a b = S b +hyper (S Z) a Z = a +hyper (S(S Z)) a Z = Z +hyper n a Z = S Z hyper (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) -------------------------------------------------------------------------------- data LTE : Nat -> Nat -> Type where - lteZero : LTE O right + lteZero : LTE Z right lteSucc : LTE left right -> LTE (S left) (S right) total GTE : Nat -> Nat -> Type @@ -71,8 +71,8 @@ total GT : Nat -> Nat -> Type GT left right = LT right left total lte : Nat -> Nat -> Bool -lte O right = True -lte left O = False +lte Z right = True +lte left Z = False lte (S left) (S right) = lte left right total gte : Nat -> Nat -> Bool @@ -103,18 +103,18 @@ maximum left right = -------------------------------------------------------------------------------- instance Eq Nat where - O == O = True + Z == Z = True (S l) == (S r) = l == r _ == _ = False instance Cast Nat Integer where - cast O = 0 + cast Z = 0 cast (S k) = 1 + cast k instance Ord Nat where - compare O O = EQ - compare O (S k) = LT - compare (S k) O = GT + compare Z Z = EQ + compare Z (S k) = LT + compare (S k) Z = GT compare (S x) (S y) = compare x y instance Num Nat where @@ -128,12 +128,12 @@ instance Num Nat where where %assert_total fromInteger' : Integer -> Nat - fromInteger' 0 = O + fromInteger' 0 = Z fromInteger' n = if (n > 0) then S (fromInteger' (n - 1)) else - O + Z instance Cast Integer Nat where cast = fromInteger @@ -171,10 +171,10 @@ instance Semigroup Additive where getAdditive m => m instance Monoid Multiplicative where - neutral = getMultiplicative $ S O + neutral = getMultiplicative $ S Z instance Monoid Additive where - neutral = getAdditive O + neutral = getAdditive Z instance MeetSemilattice Nat where meet = minimum @@ -185,14 +185,14 @@ instance JoinSemilattice Nat where instance Lattice Nat where { } instance BoundedJoinSemilattice Nat where - bottom = O + bottom = Z -------------------------------------------------------------------------------- -- Auxilliary notions -------------------------------------------------------------------------------- total pred : Nat -> Nat -pred O = O +pred Z = Z pred (S n) = n -------------------------------------------------------------------------------- @@ -200,8 +200,8 @@ pred (S n) = n -------------------------------------------------------------------------------- total fib : Nat -> Nat -fib O = O -fib (S O) = S O +fib Z = Z +fib (S Z) = S Z fib (S (S n)) = fib (S n) + fib n -------------------------------------------------------------------------------- @@ -213,11 +213,11 @@ fib (S (S n)) = fib (S n) + fib n -------------------------------------------------------------------------------- total mod : Nat -> Nat -> Nat -mod left O = left +mod left Z = left mod left (S right) = mod' left left right where total mod' : Nat -> Nat -> Nat -> Nat - mod' O centre right = centre + mod' Z centre right = centre mod' (S left) centre right = if lte centre right then centre @@ -225,21 +225,21 @@ mod left (S right) = mod' left left right mod' left (centre - (S right)) right total div : Nat -> Nat -> Nat -div left O = S left -- div by zero +div left Z = S left -- div by zero div left (S right) = div' left left right where total div' : Nat -> Nat -> Nat -> Nat - div' O centre right = O + div' Z centre right = Z div' (S left) centre right = if lte centre right then - O + Z else S (div' left (centre - (S right)) right) %assert_total log2 : Nat -> Nat -log2 O = O -log2 (S O) = O +log2 Z = Z +log2 (S Z) = Z log2 n = S (log2 (n `div` 2)) -------------------------------------------------------------------------------- @@ -260,28 +260,28 @@ total plusZeroLeftNeutral : (right : Nat) -> 0 + right = right plusZeroLeftNeutral right = refl total plusZeroRightNeutral : (left : Nat) -> left + 0 = left -plusZeroRightNeutral O = refl +plusZeroRightNeutral Z = refl plusZeroRightNeutral (S n) = let inductiveHypothesis = plusZeroRightNeutral n in ?plusZeroRightNeutralStepCase total plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + (S right) -plusSuccRightSucc O right = refl +plusSuccRightSucc Z right = refl plusSuccRightSucc (S left) right = let inductiveHypothesis = plusSuccRightSucc left right in ?plusSuccRightSuccStepCase total plusCommutative : (left : Nat) -> (right : Nat) -> left + right = right + left -plusCommutative O right = ?plusCommutativeBaseCase +plusCommutative Z right = ?plusCommutativeBaseCase plusCommutative (S left) right = let inductiveHypothesis = plusCommutative left right in ?plusCommutativeStepCase total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left + (centre + right) = (left + centre) + right -plusAssociative O centre right = refl +plusAssociative Z centre right = refl plusAssociative (S left) centre right = let inductiveHypothesis = plusAssociative left centre right in ?plusAssociativeStepCase @@ -299,38 +299,38 @@ plusOneSucc n = refl total plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) -> (p : left + right = left + right') -> right = right' -plusLeftCancel O right right' p = ?plusLeftCancelBaseCase +plusLeftCancel Z right right' p = ?plusLeftCancelBaseCase plusLeftCancel (S left) right right' p = let inductiveHypothesis = plusLeftCancel left right right' in ?plusLeftCancelStepCase total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) -> (p : left + right = left' + right) -> left = left' -plusRightCancel left left' O p = ?plusRightCancelBaseCase +plusRightCancel left left' Z p = ?plusRightCancelBaseCase plusRightCancel left left' (S right) p = let inductiveHypothesis = plusRightCancel left left' right in ?plusRightCancelStepCase total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) -> - (p : left + right = left) -> right = O -plusLeftLeftRightZero O right p = ?plusLeftLeftRightZeroBaseCase + (p : left + right = left) -> right = Z +plusLeftLeftRightZero Z right p = ?plusLeftLeftRightZeroBaseCase plusLeftLeftRightZero (S left) right p = let inductiveHypothesis = plusLeftLeftRightZero left right in ?plusLeftLeftRightZeroStepCase -- Mult -total multZeroLeftZero : (right : Nat) -> O * right = O +total multZeroLeftZero : (right : Nat) -> Z * right = Z multZeroLeftZero right = refl -total multZeroRightZero : (left : Nat) -> left * O = O -multZeroRightZero O = refl +total multZeroRightZero : (left : Nat) -> left * Z = Z +multZeroRightZero Z = refl multZeroRightZero (S left) = let inductiveHypothesis = multZeroRightZero left in ?multZeroRightZeroStepCase total multRightSuccPlus : (left : Nat) -> (right : Nat) -> left * (S right) = left + (left * right) -multRightSuccPlus O right = refl +multRightSuccPlus Z right = refl multRightSuccPlus (S left) right = let inductiveHypothesis = multRightSuccPlus left right in ?multRightSuccPlusStepCase @@ -341,40 +341,40 @@ multLeftSuccPlus left right = refl total multCommutative : (left : Nat) -> (right : Nat) -> left * right = right * left -multCommutative O right = ?multCommutativeBaseCase +multCommutative Z right = ?multCommutativeBaseCase multCommutative (S left) right = let inductiveHypothesis = multCommutative left right in ?multCommutativeStepCase total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left * (centre + right) = (left * centre) + (left * right) -multDistributesOverPlusRight O centre right = refl +multDistributesOverPlusRight Z centre right = refl multDistributesOverPlusRight (S left) centre right = let inductiveHypothesis = multDistributesOverPlusRight left centre right in ?multDistributesOverPlusRightStepCase total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) -> (left + centre) * right = (left * right) + (centre * right) -multDistributesOverPlusLeft O centre right = refl +multDistributesOverPlusLeft Z centre right = refl multDistributesOverPlusLeft (S left) centre right = let inductiveHypothesis = multDistributesOverPlusLeft left centre right in ?multDistributesOverPlusLeftStepCase total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left * (centre * right) = (left * centre) * right -multAssociative O centre right = refl +multAssociative Z centre right = refl multAssociative (S left) centre right = let inductiveHypothesis = multAssociative left centre right in ?multAssociativeStepCase total multOneLeftNeutral : (right : Nat) -> 1 * right = right -multOneLeftNeutral O = refl +multOneLeftNeutral Z = refl multOneLeftNeutral (S right) = let inductiveHypothesis = multOneLeftNeutral right in ?multOneLeftNeutralStepCase total multOneRightNeutral : (left : Nat) -> left * 1 = left -multOneRightNeutral O = refl +multOneRightNeutral Z = refl multOneRightNeutral (S left) = let inductiveHypothesis = multOneRightNeutral left in ?multOneRightNeutralStepCase @@ -384,51 +384,51 @@ total minusSuccSucc : (left : Nat) -> (right : Nat) -> (S left) - (S right) = left - right minusSuccSucc left right = refl -total minusZeroLeft : (right : Nat) -> 0 - right = O +total minusZeroLeft : (right : Nat) -> 0 - right = Z minusZeroLeft right = refl total minusZeroRight : (left : Nat) -> left - 0 = left -minusZeroRight O = refl +minusZeroRight Z = refl minusZeroRight (S left) = refl -total minusZeroN : (n : Nat) -> O = n - n -minusZeroN O = refl +total minusZeroN : (n : Nat) -> Z = n - n +minusZeroN Z = refl minusZeroN (S n) = minusZeroN n -total minusOneSuccN : (n : Nat) -> S O = (S n) - n -minusOneSuccN O = refl +total minusOneSuccN : (n : Nat) -> S Z = (S n) - n +minusOneSuccN Z = refl minusOneSuccN (S n) = minusOneSuccN n total minusSuccOne : (n : Nat) -> S n - 1 = n -minusSuccOne O = refl +minusSuccOne Z = refl minusSuccOne (S n) = refl -total minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = O -minusPlusZero O m = refl +total minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = Z +minusPlusZero Z m = refl minusPlusZero (S n) m = minusPlusZero n m total minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left - centre - right = left - (centre + right) -minusMinusMinusPlus O O right = refl -minusMinusMinusPlus (S left) O right = refl -minusMinusMinusPlus O (S centre) right = refl +minusMinusMinusPlus Z Z right = refl +minusMinusMinusPlus (S left) Z right = refl +minusMinusMinusPlus Z (S centre) right = refl minusMinusMinusPlus (S left) (S centre) right = let inductiveHypothesis = minusMinusMinusPlus left centre right in ?minusMinusMinusPlusStepCase total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) -> (left + right) - (left + right') = right - right' -plusMinusLeftCancel O right right' = refl +plusMinusLeftCancel Z right right' = refl plusMinusLeftCancel (S left) right right' = let inductiveHypothesis = plusMinusLeftCancel left right right' in ?plusMinusLeftCancelStepCase total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) -> (left - centre) * right = (left * right) - (centre * right) -multDistributesOverMinusLeft O O right = refl -multDistributesOverMinusLeft (S left) O right = +multDistributesOverMinusLeft Z Z right = refl +multDistributesOverMinusLeft (S left) Z right = ?multDistributesOverMinusLeftBaseCase -multDistributesOverMinusLeft O (S centre) right = refl +multDistributesOverMinusLeft Z (S centre) right = refl multDistributesOverMinusLeft (S left) (S centre) right = let inductiveHypothesis = multDistributesOverMinusLeft left centre right in ?multDistributesOverMinusLeftStepCase @@ -445,35 +445,35 @@ powerSuccPowerLeft base exp = refl total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) -> (power base exp) * (power base exp') = power base (exp + exp') -multPowerPowerPlus base O exp' = ?multPowerPowerPlusBaseCase +multPowerPowerPlus base Z exp' = ?multPowerPowerPlusBaseCase multPowerPowerPlus base (S exp) exp' = let inductiveHypothesis = multPowerPowerPlus base exp exp' in ?multPowerPowerPlusStepCase -total powerZeroOne : (base : Nat) -> power base 0 = S O +total powerZeroOne : (base : Nat) -> power base 0 = S Z powerZeroOne base = refl total powerOneNeutral : (base : Nat) -> power base 1 = base -powerOneNeutral O = refl +powerOneNeutral Z = refl powerOneNeutral (S base) = let inductiveHypothesis = powerOneNeutral base in ?powerOneNeutralStepCase -total powerOneSuccOne : (exp : Nat) -> power 1 exp = S O -powerOneSuccOne O = refl +total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z +powerOneSuccOne Z = refl powerOneSuccOne (S exp) = let inductiveHypothesis = powerOneSuccOne exp in ?powerOneSuccOneStepCase total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base -powerSuccSuccMult O = refl +powerSuccSuccMult Z = refl powerSuccSuccMult (S base) = let inductiveHypothesis = powerSuccSuccMult base in ?powerSuccSuccMultStepCase total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) -> power (power base exp) exp' = power base (exp * exp') -powerPowerMultPower base exp O = ?powerPowerMultPowerBaseCase +powerPowerMultPower base exp Z = ?powerPowerMultPowerBaseCase powerPowerMultPower base exp (S exp') = let inductiveHypothesis = powerPowerMultPower base exp exp' in ?powerPowerMultPowerStepCase @@ -484,9 +484,9 @@ predSucc n = refl total minusSuccPred : (left : Nat) -> (right : Nat) -> left - (S right) = pred (left - right) -minusSuccPred O right = refl -minusSuccPred (S left) O = - let inductiveHypothesis = minusSuccPred left O in +minusSuccPred Z right = refl +minusSuccPred (S left) Z = + let inductiveHypothesis = minusSuccPred left Z in ?minusSuccPredStepCase minusSuccPred (S left) (S right) = let inductiveHypothesis = minusSuccPred left right in @@ -520,69 +520,69 @@ boolElimMultMultRight False right t f = refl -- Orders total lteNTrue : (n : Nat) -> lte n n = True -lteNTrue O = refl +lteNTrue Z = refl lteNTrue (S n) = lteNTrue n -total lteSuccZeroFalse : (n : Nat) -> lte (S n) O = False -lteSuccZeroFalse O = refl +total lteSuccZeroFalse : (n : Nat) -> lte (S n) Z = False +lteSuccZeroFalse Z = refl lteSuccZeroFalse (S n) = refl -- Minimum and maximum -total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = O -minimumZeroZeroRight O = refl +total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z +minimumZeroZeroRight Z = refl minimumZeroZeroRight (S right) = minimumZeroZeroRight right -total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = O -minimumZeroZeroLeft O = refl +total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z +minimumZeroZeroLeft Z = refl minimumZeroZeroLeft (S left) = refl total minimumSuccSucc : (left : Nat) -> (right : Nat) -> minimum (S left) (S right) = S (minimum left right) -minimumSuccSucc O O = refl -minimumSuccSucc (S left) O = refl -minimumSuccSucc O (S right) = refl +minimumSuccSucc Z Z = refl +minimumSuccSucc (S left) Z = refl +minimumSuccSucc Z (S right) = refl minimumSuccSucc (S left) (S right) = let inductiveHypothesis = minimumSuccSucc left right in ?minimumSuccSuccStepCase total minimumCommutative : (left : Nat) -> (right : Nat) -> minimum left right = minimum right left -minimumCommutative O O = refl -minimumCommutative O (S right) = refl -minimumCommutative (S left) O = refl +minimumCommutative Z Z = refl +minimumCommutative Z (S right) = refl +minimumCommutative (S left) Z = refl minimumCommutative (S left) (S right) = let inductiveHypothesis = minimumCommutative left right in ?minimumCommutativeStepCase -total maximumZeroNRight : (right : Nat) -> maximum O right = right -maximumZeroNRight O = refl +total maximumZeroNRight : (right : Nat) -> maximum Z right = right +maximumZeroNRight Z = refl maximumZeroNRight (S right) = refl -total maximumZeroNLeft : (left : Nat) -> maximum left O = left -maximumZeroNLeft O = refl +total maximumZeroNLeft : (left : Nat) -> maximum left Z = left +maximumZeroNLeft Z = refl maximumZeroNLeft (S left) = refl total maximumSuccSucc : (left : Nat) -> (right : Nat) -> S (maximum left right) = maximum (S left) (S right) -maximumSuccSucc O O = refl -maximumSuccSucc (S left) O = refl -maximumSuccSucc O (S right) = refl +maximumSuccSucc Z Z = refl +maximumSuccSucc (S left) Z = refl +maximumSuccSucc Z (S right) = refl maximumSuccSucc (S left) (S right) = let inductiveHypothesis = maximumSuccSucc left right in ?maximumSuccSuccStepCase total maximumCommutative : (left : Nat) -> (right : Nat) -> maximum left right = maximum right left -maximumCommutative O O = refl -maximumCommutative (S left) O = refl -maximumCommutative O (S right) = refl +maximumCommutative Z Z = refl +maximumCommutative (S left) Z = refl +maximumCommutative Z (S right) = refl maximumCommutative (S left) (S right) = let inductiveHypothesis = maximumCommutative left right in ?maximumCommutativeStepCase -- div and mod -total modZeroZero : (n : Nat) -> mod 0 n = O -modZeroZero O = refl +total modZeroZero : (n : Nat) -> mod 0 n = Z +modZeroZero Z = refl modZeroZero (S n) = refl -------------------------------------------------------------------------------- @@ -613,7 +613,7 @@ powerSuccSuccMultStepCase = proof { powerOneSuccOneStepCase = proof { intros; rewrite inductiveHypothesis; - rewrite sym (plusZeroRightNeutral (power (S O) exp)); + rewrite sym (plusZeroRightNeutral (power (S Z) exp)); trivial; } diff --git a/lib/Prelude/Vect.idr b/lib/Prelude/Vect.idr index de72ac13e..278bb892b 100644 --- a/lib/Prelude/Vect.idr +++ b/lib/Prelude/Vect.idr @@ -10,7 +10,7 @@ import Prelude.Nat infixr 7 :: data Vect : Type -> Nat -> Type where - Nil : Vect a O + Nil : Vect a Z (::) : a -> Vect a n -> Vect a (S n) -------------------------------------------------------------------------------- @@ -81,7 +81,7 @@ fromList (x::xs) = x :: fromList xs (++) (x::xs) ys = x :: xs ++ ys replicate : (n : Nat) -> a -> Vect a n -replicate O x = [] +replicate Z x = [] replicate (S k) x = x :: replicate k x -------------------------------------------------------------------------------- @@ -322,7 +322,7 @@ range = reverse range_ where range_ : Vect (Fin n) n - range_ {n=O} = Nil + range_ {n=Z} = Nil range_ {n=(S _)} = last :: map weaken range_ -------------------------------------------------------------------------------- diff --git a/lib/Uninhabited.idr b/lib/Uninhabited.idr index 799b1f07f..32a806e5d 100644 --- a/lib/Uninhabited.idr +++ b/lib/Uninhabited.idr @@ -3,10 +3,10 @@ module Uninhabited class Uninhabited t where total uninhabited : t -> _|_ -instance Uninhabited (Fin O) where +instance Uninhabited (Fin Z) where uninhabited fO impossible uninhabited (fS f) impossible -instance Uninhabited (O = S n) where +instance Uninhabited (Z = S n) where uninhabited refl impossible diff --git a/samples/binary.idr b/samples/binary.idr index 143b9089a..06ba293a3 100644 --- a/samples/binary.idr +++ b/samples/binary.idr @@ -11,7 +11,7 @@ instance Show (Bit n) where infixl 5 # data Binary : (width : Nat) -> (value : Nat) -> Type where - zero : Binary O O + zero : Binary Z Z (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v) instance Show (Binary w k) where @@ -83,7 +83,7 @@ main.adc_lemma_2 = proof { rewrite sym (plusAssociative x v v1); rewrite sym (plusCommutative (plus (plus x v) v1) v1); rewrite plusZeroRightNeutral (plus (plus x v) v1); - rewrite sym (plusAssociative (plus x v) v1 (plus (plus (plus x v) v1) O)); + rewrite sym (plusAssociative (plus x v) v1 (plus (plus (plus x v) v1) Z)); trivial; } diff --git a/src/IRTS/Compiler.hs b/src/IRTS/Compiler.hs index 7a593b659..c8c09557e 100644 --- a/src/IRTS/Compiler.hs +++ b/src/IRTS/Compiler.hs @@ -237,7 +237,7 @@ instance ToIR (TT Name) where where mkUnused u i [] = [] mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs | otherwise = x : mkUnused u (i + 1) xs --- ir' env (P _ (NS (UN "O") ["Nat", "Prelude"]) _) +-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _) -- = return $ LConst (BI 0) ir' env (P _ n _) = return $ LV (Glob n) ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i)) @@ -331,7 +331,7 @@ mkIntIty "IT16" = FArith (ATInt (ITFixed IT16)) mkIntIty "IT32" = FArith (ATInt (ITFixed IT32)) mkIntIty "IT64" = FArith (ATInt (ITFixed IT64)) -zname = NS (UN "O") ["Nat","Prelude"] +zname = NS (UN "Z") ["Nat","Prelude"] sname = NS (UN "S") ["Nat","Prelude"] instance ToIR ([Name], SC) where @@ -351,7 +351,7 @@ instance ToIR SC where return $ LCase (LV (Glob n)) alts' ir' ImpossibleCase = return LNothing - -- special cases for O and S + -- special cases for Z and S -- Needs rethink: projections make this fail -- mkIRAlt n (ConCase z _ [] rhs) | z == zname -- = mkIRAlt n (ConstCase (BI 0) rhs) diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs index b84a00c05..6550879e1 100644 --- a/src/Idris/AbsSyntaxTree.hs +++ b/src/Idris/AbsSyntaxTree.hs @@ -1128,10 +1128,10 @@ showImp impl tm = se 10 tm where xs -> "[" ++ intercalate "," (map (se p) xs) ++ "]" slist _ _ = Nothing - -- since Prelude is always imported, S & O are unqualified iff they're the + -- since Prelude is always imported, S & Z are unqualified iff they're the -- Nat ones. snat p (PRef _ o) - | show o == (natns++"O") || show o == "O" = Just 0 + | show o == (natns++"Z") || show o == "Z" = Just 0 snat p (PApp _ s [PExp {getTm=n}]) | show s == (natns++"S") || show s == "S", Just n' <- snat p n diff --git a/src/Idris/Transforms.hs b/src/Idris/Transforms.hs index a94c882f3..afc65a0e1 100644 --- a/src/Idris/Transforms.hs +++ b/src/Idris/Transforms.hs @@ -39,7 +39,7 @@ instance Transform CaseAlt where natTrans = [TermTrans zero, TermTrans suc, CaseTrans natcase] -zname = NS (UN "O") ["Nat","Prelude"] +zname = NS (UN "Z") ["Nat","Prelude"] sname = NS (UN "S") ["Nat","Prelude"] zero :: TT Name -> TT Name diff --git a/test/reg001/reg001.idr b/test/reg001/reg001.idr index e732ea12c..6dd29ae62 100644 --- a/test/reg001/reg001.idr +++ b/test/reg001/reg001.idr @@ -8,4 +8,4 @@ data Imp : Type where MkImp : {any : Type} -> any -> Imp testVal : Imp -testVal = MkImp (apply id O) +testVal = MkImp (apply id Z) diff --git a/test/reg004/reg004.idr b/test/reg004/reg004.idr index 36712f23d..97be01f02 100644 --- a/test/reg004/reg004.idr +++ b/test/reg004/reg004.idr @@ -3,12 +3,12 @@ module Main h : Bool -> Nat h False = r1 where r : Nat - r = S O + r = S Z r1 : Nat r1 = r h True = r2 where r : Nat - r = O + r = Z r2 : Nat r2 = r diff --git a/test/reg005/reg005.idr b/test/reg005/reg005.idr index a25785381..17be18988 100644 --- a/test/reg005/reg005.idr +++ b/test/reg005/reg005.idr @@ -1,7 +1,7 @@ module Main rep : (n : Nat) -> Char -> Vect Char n -rep O x = [] +rep Z x = [] rep (S k) x = x :: rep k x data RLE : Vect Char n -> Type where @@ -18,12 +18,12 @@ eq x y = if x == y then Just ?eqCharOK else Nothing rle : (xs : Vect Char n) -> RLE xs rle [] = REnd rle (x :: xs) with (rle xs) - rle (x :: Vect.Nil) | REnd = RChar O x REnd + rle (x :: Vect.Nil) | REnd = RChar Z x REnd rle (x :: rep (S n) yvar ++ ys) | RChar n yvar rs with (eq x yvar) rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just refl = RChar (S n) x rs rle (x :: rep (S n) y ++ ys) | RChar n y rs | Nothing - = RChar O x (RChar n y rs) + = RChar Z x (RChar n y rs) compress : Vect Char n -> String compress xs with (rle xs) diff --git a/test/reg006/reg006.idr b/test/reg006/reg006.idr index 36000eace..b93bf411d 100644 --- a/test/reg006/reg006.idr +++ b/test/reg006/reg006.idr @@ -3,7 +3,7 @@ module RBTree data Colour = Red | Black data RBTree : Type -> Type -> Nat -> Colour -> Type where - Leaf : RBTree k v O Black + Leaf : RBTree k v Z Black RedBranch : k -> v -> RBTree k v n Black -> RBTree k v n Black -> RBTree k v n Red BlackBranch : k -> v -> RBTree k v n x -> RBTree k v n y -> RBTree k v (S n) Black diff --git a/test/reg008/reg008.idr b/test/reg008/reg008.idr index a50c3e703..3b33589e0 100644 --- a/test/reg008/reg008.idr +++ b/test/reg008/reg008.idr @@ -6,9 +6,9 @@ data Cmp : Nat -> Nat -> Type where cmpGT : (x : _) -> Cmp (y + S x) y total cmp : (x, y : Nat) -> Cmp x y -cmp O O = cmpEQ -cmp O (S k) = cmpLT _ -cmp (S k) O = cmpGT _ +cmp Z Z = cmpEQ +cmp Z (S k) = cmpLT _ +cmp (S k) Z = cmpGT _ cmp (S x) (S y) with (cmp x y) cmp (S x) (S (x + (S k))) | cmpLT k = cmpLT k cmp (S x) (S x) | cmpEQ = cmpEQ diff --git a/test/reg009/reg009.lidr b/test/reg009/reg009.lidr index 4f7144639..50a242eab 100644 --- a/test/reg009/reg009.lidr +++ b/test/reg009/reg009.lidr @@ -6,7 +6,7 @@ > filterTagP : (p : alpha -> Bool) -> > (as : Vect alpha n) -> > so (isAnyBy p (n ** as)) -> -> (m : Nat ** (Vect (a : alpha ** so (p a)) m, so (m > O))) +> (m : Nat ** (Vect (a : alpha ** so (p a)) m, so (m > Z))) > filterTagP {n = S m} p (a :: as) q with (p a) > | True = (_ > ** diff --git a/test/reg010/reg010.idr b/test/reg010/reg010.idr index 8c2ab8433..8aae03a60 100644 --- a/test/reg010/reg010.idr +++ b/test/reg010/reg010.idr @@ -1,5 +1,5 @@ module usubst total unsafeSubst : (P : a -> Type) -> (x : a) -> (y : a) -> P x -> P y -unsafeSubst P x y px with (O) +unsafeSubst P x y px with (Z) unsafeSubst P x x px | _ = px diff --git a/test/reg011/reg011.idr b/test/reg011/reg011.idr index 4609a413c..9504add09 100644 --- a/test/reg011/reg011.idr +++ b/test/reg011/reg011.idr @@ -1,9 +1,9 @@ vfoldl : (P : Nat -> Type) -> - ((x : Nat) -> P x -> a -> P (S x)) -> P O + ((x : Nat) -> P x -> a -> P (S x)) -> P Z -> Vect a m -> P m -- vfoldl P cons nil [] -- = nil vfoldl P cons nil (x :: xs) - = vfoldl (\k => P (S k)) (\ n => cons (S n)) (cons O nil x) xs + = vfoldl (\k => P (S k)) (\ n => cons (S n)) (cons Z nil x) xs -- vfoldl P cons nil (x :: xs) -- = vfoldl (\n => P (S n)) (\ n => cons _) (cons _ nil x) xs diff --git a/test/reg018/reg018b.idr b/test/reg018/reg018b.idr index c6037a74e..5730b7887 100644 --- a/test/reg018/reg018b.idr +++ b/test/reg018/reg018b.idr @@ -2,13 +2,13 @@ module A %default total -codata B = O B | I B +codata B = Z B | I B showB : B -> String showB (I x) = "I" ++ showB x -showB (O x) = "O" ++ showB x +showB (Z x) = "Z" ++ showB x instance Show B where show = showB os : B -os = O os +os = Z os diff --git a/test/reg018/reg018c.idr b/test/reg018/reg018c.idr index 2f2e43f77..d49d47dc7 100644 --- a/test/reg018/reg018c.idr +++ b/test/reg018/reg018c.idr @@ -9,7 +9,7 @@ codata InfStream a = (::) a (InfStream a) -- natFromStream n = (::) n (natFromStream (S n)) take : (n: Nat) -> InfStream a -> Vect a n -take O _ = [] +take Z _ = [] take (S n) (x :: xs) = x :: take n xs hdtl : InfStream a -> (a, InfStream a) diff --git a/test/reg018/reg018d.idr b/test/reg018/reg018d.idr index aada90d3e..6550ed57f 100644 --- a/test/reg018/reg018d.idr +++ b/test/reg018/reg018d.idr @@ -2,7 +2,7 @@ module Main total pull : Fin (S n) -> Vect a (S n) -> (a, Vect a n) -pull {n=O} _ (x :: xs) = (x, xs) +pull {n=Z} _ (x :: xs) = (x, xs) -- pull {n=S q} fO (Vect.(::) {n=S _} x xs) = (x, xs) pull {n=S _} (fS n) (x :: xs) = let (v, vs) = pull n xs in diff --git a/test/test005/test005.idr b/test/test005/test005.idr index c9c70ee65..926f78d72 100644 --- a/test/test005/test005.idr +++ b/test/test005/test005.idr @@ -8,7 +8,7 @@ tlist = [1, 2, 3, 4, 5] main : IO () main = do print (abs (-8)) - print (abs (S O)) + print (abs (S Z)) print (span isAlpha tstr) print (break isDigit tstr) print (span (\x => x < 3) tlist) diff --git a/test/test006/test006.idr b/test/test006/test006.idr index dcb9ef776..590b8065e 100644 --- a/test/test006/test006.idr +++ b/test/test006/test006.idr @@ -5,14 +5,14 @@ data Parity : Nat -> Type where odd : Parity (S (n + n)) parity : (n:Nat) -> Parity n -parity O = even {n=O} -parity (S O) = odd {n=O} +parity Z = even {n=Z} +parity (S Z) = odd {n=Z} parity (S (S k)) with (parity k) parity (S (S (j + j))) | (even {n = j}) ?= even {n=S j} parity (S (S (S (j + j)))) | (odd {n = j}) ?= odd {n=S j} natToBin : Nat -> List Bool -natToBin O = Nil +natToBin Z = Nil natToBin k with (parity k) natToBin (j + j) | even {n = j} = False :: natToBin j natToBin (S (j + j)) | odd {n = j} = True :: natToBin j diff --git a/test/test015/Parity.idr b/test/test015/Parity.idr index b742dfc51..98e8b7224 100644 --- a/test/test015/Parity.idr +++ b/test/test015/Parity.idr @@ -5,8 +5,8 @@ data Parity : Nat -> Type where odd : Parity (S (n + n)) parity : (n:Nat) -> Parity n -parity O = even {n=O} -parity (S O) = odd {n=O} +parity Z = even {n=Z} +parity (S Z) = odd {n=Z} parity (S (S k)) with (parity k) parity (S (S (j + j))) | even ?= even {n=S j} parity (S (S (S (j + j)))) | odd ?= odd {n=S j} diff --git a/test/test015/test015.idr b/test/test015/test015.idr index a258621d7..ca8cd9a3d 100644 --- a/test/test015/test015.idr +++ b/test/test015/test015.idr @@ -4,8 +4,8 @@ import Parity import System data Bit : Nat -> Type where - b0 : Bit O - b1 : Bit (S O) + b0 : Bit Z + b1 : Bit (S Z) instance Show (Bit n) where show = show' where @@ -16,7 +16,7 @@ instance Show (Bit n) where infixl 5 # data Binary : (width : Nat) -> (value : Nat) -> Type where - zero : Binary O O + zero : Binary Z Z (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v) instance Show (Binary w k) where @@ -29,9 +29,9 @@ pad (num # x) = pad num # x natToBin : (width : Nat) -> (n : Nat) -> Maybe (Binary width n) -natToBin O (S k) = Nothing -natToBin O O = Just zero -natToBin (S k) O = do x <- natToBin k O +natToBin Z (S k) = Nothing +natToBin Z Z = Just zero +natToBin (S k) Z = do x <- natToBin k Z Just (pad x) natToBin (S w) (S k) with (parity k) natToBin (S w) (S (plus j j)) | even = do jbin <- natToBin w j diff --git a/test/test016/test016.idr b/test/test016/test016.idr index f68fe67cf..bcda2c6f8 100644 --- a/test/test016/test016.idr +++ b/test/test016/test016.idr @@ -8,7 +8,7 @@ countFrom : Int -> Stream Int countFrom x = x :: countFrom (x + 1) take : Nat -> Stream a -> List a -take O _ = [] +take Z _ = [] take (S n) (x :: xs) = x :: take n xs take n [] = [] diff --git a/test/test017/test017.idr b/test/test017/test017.idr index 781bfeea8..b69d714a4 100644 --- a/test/test017/test017.idr +++ b/test/test017/test017.idr @@ -5,8 +5,8 @@ module scg data Ord = Zero | Suc Ord | Sup (Nat -> Ord) natElim : (n : Nat) -> (P : Nat -> Type) -> - (P O) -> ((n : Nat) -> (P n) -> (P (S n))) -> (P n) -natElim O P mO mS = mO + (P Z) -> ((n : Nat) -> (P n) -> (P (S n))) -> (P n) +natElim Z P mO mS = mO natElim (S k) P mO mS = mS k (natElim k P mO mS) ordElim : (x : Ord) -> @@ -23,10 +23,10 @@ ordElim (Sup f) P mZ mSuc mSup = myplus' : Nat -> Nat -> Nat myplus : Nat -> Nat -> Nat -myplus O y = y +myplus Z y = y myplus (S k) y = S (myplus' k y) -myplus' O y = y +myplus' Z y = y myplus' (S k) y = S (myplus y k) mnubBy : (a -> a -> Bool) -> List a -> List a @@ -46,23 +46,23 @@ vtrans [] _ = [] vtrans (x :: xs) ys = x :: vtrans ys ys even : Nat -> Bool -even O = True +even Z = True even (S k) = odd k where odd : Nat -> Bool - odd O = False + odd Z = False odd (S k) = even k ack : Nat -> Nat -> Nat -ack O n = S n -ack (S m) O = ack m (S O) +ack Z n = S n +ack (S m) Z = ack m (S Z) ack (S m) (S n) = ack m (ack (S m) n) data Bin = eps | c0 Bin | c1 Bin foo : Bin -> Nat -foo eps = O -foo (c0 eps) = O +foo eps = Z +foo (c0 eps) = Z foo (c0 (c1 x)) = S (foo (c1 x)) foo (c0 (c0 x)) = foo (c0 x) foo (c1 x) = S (foo x) @@ -70,19 +70,19 @@ foo (c1 x) = S (foo x) bar : Nat -> Nat -> Nat bar x y = mp x y where mp : Nat -> Nat -> Nat - mp O y = y + mp Z y = y mp (S k) y = S (bar k y) total mfib : Nat -> Nat -mfib O = O -mfib (S O) = S O +mfib Z = Z +mfib (S Z) = S Z mfib (S (S n)) = mfib (S n) + mfib n maxCommutative : (left : Nat) -> (right : Nat) -> maximum left right = maximum right left -maxCommutative O O = refl -maxCommutative (S left) O = refl -maxCommutative O (S right) = refl +maxCommutative Z Z = refl +maxCommutative (S left) Z = refl +maxCommutative Z (S right) = refl maxCommutative (S left) (S right) = let inductiveHypothesis = maxCommutative left right in ?maxCommutativeStepCase diff --git a/test/test019/test019.lidr b/test/test019/test019.lidr index 2761f3421..cb64f154c 100644 --- a/test/test019/test019.lidr +++ b/test/test019/test019.lidr @@ -1,7 +1,7 @@ > module Main > ifTrue : so True -> Nat -> ifTrue oh = S O +> ifTrue oh = S Z > ifFalse : so False -> Nat > ifFalse oh impossible diff --git a/test/test025/test025.idr b/test/test025/test025.idr index 9b0e61f85..428cda752 100644 --- a/test/test025/test025.idr +++ b/test/test025/test025.idr @@ -21,9 +21,9 @@ testMemory = do Src :- allocate 5 Dst :- initialize (prim__truncInt_B8 1) 2 oh move 2 2 3 oh oh Src :- free - end <- Dst :- peek 4 (S O) oh + end <- Dst :- peek 4 (S Z) oh Dst :- poke 4 (sub1 end) oh - res <- Dst :- peek 1 (S(S(S(S O)))) oh + res <- Dst :- peek 1 (S(S(S(S Z)))) oh Dst :- free return (map (prim__zextB8_Int) res) diff --git a/tutorial/classes.tex b/tutorial/classes.tex index caec293c2..370778c8d 100644 --- a/tutorial/classes.tex +++ b/tutorial/classes.tex @@ -43,10 +43,10 @@ could be defined as: \begin{SaveVerbatim}{shownat} instance Show Nat where - show O = "O" + show Z = "Z" show (S k) = "s" ++ show k -Idris> show (S (S (S O))) +Idris> show (S (S (S Z))) "sssO" : String \end{SaveVerbatim} @@ -101,10 +101,10 @@ For example, for an instance of \texttt{Eq} for \texttt{Nat}: \begin{SaveVerbatim}{eqnat} instance Eq Nat where - O == O = True + Z == Z = True (S x) == (S y) = x == y - O == (S y) = False - (S x) == O = False + Z == (S y) = False + (S x) == Z = False x /= y = not (x == y) @@ -498,9 +498,9 @@ be \remph{named} as follows: \begin{SaveVerbatim}{myord} instance [myord] Ord Nat where - compare O (S n) = GT - compare (S n) O = LT - compare O O = EQ + compare Z (S n) = GT + compare (S n) Z = LT + compare Z Z = EQ compare (S x) (S y) = compare @{myord} x y \end{SaveVerbatim} diff --git a/tutorial/examples/binary.idr b/tutorial/examples/binary.idr index b0ae32f96..4712814fc 100644 --- a/tutorial/examples/binary.idr +++ b/tutorial/examples/binary.idr @@ -1,7 +1,7 @@ module Main data Binary : Nat -> Type where - bEnd : Binary O + bEnd : Binary Z bO : Binary n -> Binary (n + n) bI : Binary n -> Binary (S (n + n)) @@ -15,21 +15,21 @@ data Parity : Nat -> Type where odd : Parity (S (n + n)) parity : (n:Nat) -> Parity n -parity O = even {n=O} -parity (S O) = odd {n=O} +parity Z = even {n=Z} +parity (S Z) = odd {n=Z} parity (S (S k)) with (parity k) parity (S (S (j + j))) | even ?= even {n=S j} parity (S (S (S (j + j)))) | odd ?= odd {n=S j} natToBin : (n:Nat) -> Binary n -natToBin O = bEnd +natToBin Z = bEnd natToBin (S k) with (parity k) natToBin (S (j + j)) | even = bI (natToBin j) natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j)) intToNat : Int -> Nat -intToNat 0 = O -intToNat x = if (x>0) then (S (intToNat (x-1))) else O +intToNat 0 = Z +intToNat x = if (x>0) then (S (intToNat (x-1))) else Z main : IO () main = do putStr "Enter a number: " diff --git a/tutorial/examples/theorems.idr b/tutorial/examples/theorems.idr index a0df7f437..a2ceef849 100644 --- a/tutorial/examples/theorems.idr +++ b/tutorial/examples/theorems.idr @@ -5,15 +5,15 @@ fiveIsFive = refl twoPlusTwo : 2 + 2 = 4 twoPlusTwo = refl -total disjoint : (n : Nat) -> O = S n -> _|_ +total disjoint : (n : Nat) -> Z = S n -> _|_ disjoint n p = replace {P = disjointTy} p () where disjointTy : Nat -> Type - disjointTy O = () + disjointTy Z = () disjointTy (S k) = _|_ total acyclic : (n : Nat) -> n = S n -> _|_ -acyclic O p = disjoint _ p +acyclic Z p = disjoint _ p acyclic (S k) p = acyclic k (succInjective _ _ p) empty1 : _|_ @@ -24,33 +24,33 @@ empty1 = hd [] where empty2 : _|_ empty2 = empty2 -plusReduces : (n:Nat) -> plus O n = n +plusReduces : (n:Nat) -> plus Z n = n plusReduces n = refl -plusReducesO : (n:Nat) -> n = plus n O -plusReducesO O = refl -plusReducesO (S k) = cong (plusReducesO k) +plusReducesZ : (n:Nat) -> n = plus n Z +plusReducesZ Z = refl +plusReducesZ (S k) = cong (plusReducesZ k) plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m) -plusReducesS O m = refl +plusReducesS Z m = refl plusReducesS (S k) m = cong (plusReducesS k m) -plusReducesO' : (n:Nat) -> n = plus n O -plusReducesO' O = ?plusredO_O -plusReducesO' (S k) = let ih = plusReducesO' k in - ?plusredO_S +plusReducesZ' : (n:Nat) -> n = plus n Z +plusReducesZ' Z = ?plusredZ_Z +plusReducesZ' (S k) = let ih = plusReducesZ' k in + ?plusredZ_S ---------- Proofs ---------- -plusredO_S = proof { +plusredZ_S = proof { intro; intro; rewrite ih; trivial; } -plusredO_O = proof { +plusredZ_Z = proof { compute; trivial; } diff --git a/tutorial/examples/usefultypes.idr b/tutorial/examples/usefultypes.idr index f93603b99..3d996a970 100644 --- a/tutorial/examples/usefultypes.idr +++ b/tutorial/examples/usefultypes.idr @@ -10,7 +10,7 @@ vec = (_ ** [3, 4]) list_lookup : Nat -> List a -> Maybe a list_lookup _ Nil = Nothing -list_lookup O (x :: xs) = Just x +list_lookup Z (x :: xs) = Just x list_lookup (S k) (x :: xs) = list_lookup k xs lookup_default : Nat -> List a -> a -> a diff --git a/tutorial/examples/views.idr b/tutorial/examples/views.idr index 71ac8a83a..90198f9dc 100644 --- a/tutorial/examples/views.idr +++ b/tutorial/examples/views.idr @@ -5,14 +5,14 @@ data Parity : Nat -> Type where odd : Parity (S (n + n)) parity : (n:Nat) -> Parity n -parity O = even {n=O} -parity (S O) = odd {n=O} +parity Z = even {n=Z} +parity (S Z) = odd {n=Z} parity (S (S k)) with (parity k) parity (S (S (j + j))) | even ?= even {n=S j} parity (S (S (S (j + j)))) | odd ?= odd {n=S j} natToBin : Nat -> List Bool -natToBin O = Nil +natToBin Z = Nil natToBin k with (parity k) natToBin (j + j) | even = False :: natToBin j natToBin (S (j + j)) | odd = True :: natToBin j diff --git a/tutorial/examples/wheres.idr b/tutorial/examples/wheres.idr index b771d7db2..ec7aa1acb 100644 --- a/tutorial/examples/wheres.idr +++ b/tutorial/examples/wheres.idr @@ -1,13 +1,13 @@ module wheres even : Nat -> Bool -even O = True +even Z = True even (S k) = odd k where - odd O = False + odd Z = False odd (S k) = even k test : List Nat -test = [c (S 1), c O, d (S O)] +test = [c (S 1), c Z, d (S Z)] where c x = 42 + x d y = c (y + 1 + z y) where z w = y + w diff --git a/tutorial/provisional.tex b/tutorial/provisional.tex index c3dde79a2..d3d5fe982 100644 --- a/tutorial/provisional.tex +++ b/tutorial/provisional.tex @@ -22,8 +22,8 @@ We'd like to implement this as follows: \begin{SaveVerbatim}{parfail} parity : (n:Nat) -> Parity n -parity O = even {n=O} -parity (S O) = odd {n=O} +parity Z = even {n=Z} +parity (S Z) = odd {n=Z} parity (S (S k)) with (parity k) parity (S (S (j + j))) | even = even {n=S j} 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 \begin{SaveVerbatim}{paritypro} parity : (n:Nat) -> Parity n -parity O = even {n=O} -parity (S O) = odd {n=O} +parity Z = even {n=Z} +parity (S Z) = odd {n=Z} parity (S (S k)) with (parity k) parity (S (S (j + j))) | even ?= even {n=S j} parity (S (S (S (j + j)))) | odd ?= odd {n=S j} @@ -231,7 +231,7 @@ case \texttt{Nat}): \begin{SaveVerbatim}{bindef} data Binary : Nat -> Type where - bEnd : Binary O + bEnd : Binary Z bO : Binary n -> Binary (n + n) bI : Binary n -> Binary (S (n + n)) @@ -263,7 +263,7 @@ provisional definition in the odd case: \begin{SaveVerbatim}{ntbdef} natToBin : (n:Nat) -> Binary n -natToBin O = bEnd +natToBin Z = bEnd natToBin (S k) with (parity k) natToBin (S (j + j)) | even = bI (natToBin j) natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j)) diff --git a/tutorial/theorems.tex b/tutorial/theorems.tex index fdfb47cc8..d6bbad0ae 100644 --- a/tutorial/theorems.tex +++ b/tutorial/theorems.tex @@ -42,11 +42,11 @@ to a successor: \begin{SaveVerbatim}{natdisjoint} -disjoint : (n : Nat) -> O = S n -> _|_ +disjoint : (n : Nat) -> Z = S n -> _|_ disjoint n p = replace {P = disjointTy} p () where disjointTy : Nat -> Type - disjointTy O = () + disjointTy Z = () disjointTy (S k) = _|_ \end{SaveVerbatim} @@ -76,7 +76,7 @@ we want to prove the following theorem about the reduction behaviour of \texttt{ \begin{SaveVerbatim}{plusred} -plusReduces : (n:Nat) -> plus O n = n +plusReduces : (n:Nat) -> plus Z n = n \end{SaveVerbatim} \useverb{plusred} @@ -90,7 +90,7 @@ of interest. We won't go into details here, but the Curry-Howard correspondence~\cite{howard} explains this relationship. -The proof itself is trivial, because \texttt{plus O n} normalises to \texttt{n} +The proof itself is trivial, because \texttt{plus Z n} normalises to \texttt{n} by the definition of \texttt{plus}: \begin{SaveVerbatim}{plusredp} @@ -107,9 +107,9 @@ on the first argument to \texttt{plus}, namely \texttt{n}. \begin{SaveVerbatim}{plusRedO} -plusReducesO : (n:Nat) -> n = plus n O -plusReducesO O = refl -plusReducesO (S k) = cong (plusReducesO k) +plusReducesZ : (n:Nat) -> n = plus n Z +plusReducesZ Z = refl +plusReducesZ (S k) = cong (plusReducesZ k) \end{SaveVerbatim} \useverb{plusRedO} @@ -131,7 +131,7 @@ We can do the same for the reduction behaviour of plus on successors: \begin{SaveVerbatim}{plusRedS} plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m) -plusReducesS O m = refl +plusReducesS Z m = refl plusReducesS (S k) m = cong (plusReducesS k m) \end{SaveVerbatim} @@ -148,16 +148,16 @@ therefore provides an interactive proof mode. Instead of writing the proof in one go, we can use \Idris{}'s interactive proof mode. To do this, we write the general \emph{structure} of the proof, and use the interactive mode to complete the details. We'll be constructing -the proof by \emph{induction}, so we write the cases for \texttt{O} and +the proof by \emph{induction}, so we write the cases for \texttt{Z} and \texttt{S}, with a recursive call in the \texttt{S} case giving the inductive hypothesis, and insert \emph{metavariables} for the rest of the definition: \begin{SaveVerbatim}{prOstruct} -plusReducesO' : (n:Nat) -> n = plus n O -plusReducesO' O = ?plusredO_O -plusReducesO' (S k) = let ih = plusReducesO' k in - ?plusredO_S +plusReducesZ' : (n:Nat) -> n = plus n Z +plusReducesZ' Z = ?plusredZ_Z +plusReducesZ' (S k) = let ih = plusReducesZ' k in + ?plusredZ_S \end{SaveVerbatim} \useverb{prOstruct} @@ -173,17 +173,17 @@ precisely, which functions exist but have no definitions), then the *theorems> :m Global metavariables: - [plusredO_S,plusredO_O] + [plusredZ_S,plusredZ_Z] \end{SaveVerbatim} \begin{SaveVerbatim}{metatypes} -*theorems> :t plusredO_O -plusredO_O : O = plus O O +*theorems> :t plusredZ_Z +plusredZ_Z : Z = plus Z Z -*theorems> :t plusredO_S -plusredO_S : (k : Nat) -> (k = plus k O) -> S k = S (plus k O) +*theorems> :t plusredZ_S +plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = S (plus k Z) \end{SaveVerbatim} \useverb{showmetas} @@ -196,10 +196,10 @@ the missing definitions. \begin{SaveVerbatim}{proveO} -*theorems> :p plusredO_O +*theorems> :p plusredZ_Z ----------------------------------- (plusredO_O) -------- -{hole0} : O = plus O O +---------------------------------- (plusredZ_Z) -------- +{hole0} : Z = plus Z Z \end{SaveVerbatim} \useverb{proveO} @@ -213,24 +213,24 @@ we can normalise the goal with the \texttt{compute} tactic: \begin{SaveVerbatim}{compute} --plusredO_O> compute +-plusredZ_Z> compute ----------------------------------- (plusredO_O) -------- -{hole0} : O = O +---------------------------------- (plusredZ_Z) -------- +{hole0} : Z = Z \end{SaveVerbatim} \useverb{compute} \noindent -Now we have to prove that \texttt{O} equals \texttt{O}, which is easy to prove by +Now we have to prove that \texttt{Z} equals \texttt{Z}, which is easy to prove by \texttt{refl}. To apply a function, such as \texttt{refl}, we use \texttt{refine} which introduces subgoals for each of the function's explicit arguments (\texttt{refl} has none): \begin{SaveVerbatim}{refrefl} --plusredO_O> refine refl -plusredO_O: no more goals +-plusredZ_Z> refine refl +plusredZ_Z: no more goals \end{SaveVerbatim} \useverb{refrefl} @@ -244,8 +244,8 @@ This also outputs a trace of the proof: \begin{SaveVerbatim}{prOprooftrace} --plusredO_O> qed -plusredO_O = proof { +-plusredZ_Z> qed +plusredZ_Z = proof { compute; refine refl; } @@ -257,7 +257,7 @@ plusredO_O = proof { *theorems> :m Global metavariables: - [plusredO_S] + [plusredZ_S] \end{SaveVerbatim} \useverb{showmetasO} @@ -269,10 +269,10 @@ Let us now prove the other required lemma, \texttt{plusredO\_S}: \begin{SaveVerbatim}{plusredOSprf} -*theorems> :p plusredO_S +*theorems> :p plusredZ_S ----------------------------------- (plusredO_S) -------- -{hole0} : (k : Nat) -> (k = plus k O) -> S k = S (plus k O) +---------------------------------- (plusredZ_S) -------- +{hole0} : (k : Nat) -> (k = plus k Z) -> S k = S (plus k Z) \end{SaveVerbatim} \useverb{plusredOSprf} @@ -286,28 +286,28 @@ twice (or \texttt{intros}, which introduces all arguments as premisses). This gi \begin{SaveVerbatim}{prSintros} k : Nat - ih : k = plus k O ----------------------------------- (plusredO_S) -------- -{hole2} : S k = S (plus k O) + ih : k = plus k Z +---------------------------------- (plusredZ_S) -------- +{hole2} : S k = S (plus k Z) \end{SaveVerbatim} \useverb{prSintros} \noindent -We know, from the type of \texttt{ih}, that \texttt{k = plus k O}, so we would like to -use this knowledge to replace \texttt{plus k O} in the goal with \texttt{k}. We can +We know, from the type of \texttt{ih}, that \texttt{k = plus k Z}, so we would like to +use this knowledge to replace \texttt{plus k Z} in the goal with \texttt{k}. We can achieve this with the \texttt{rewrite} tactic: \begin{SaveVerbatim}{} --plusredO_S> rewrite ih +-plusredZ_S> rewrite ih k : Nat - ih : k = plus k O ----------------------------------- (plusredO_S) -------- + ih : k = plus k Z +---------------------------------- (plusredZ_S) -------- {hole3} : S k = S k --plusredO_S> +-plusredZ_S> \end{SaveVerbatim} \useverb{} @@ -318,10 +318,10 @@ the goal using that proof. Here, it results in an equality which is trivially pr \begin{SaveVerbatim}{prOStrace} --plusredO_S> trivial -plusredO_S: no more goals --plusredO_S> qed -plusredO_S = proof { +-plusredZ_S> trivial +plusredZ_S: no more goals +-plusredZ_S> qed +plusredZ_S = proof { intros; rewrite ih; trivial; diff --git a/tutorial/typesfuns.tex b/tutorial/typesfuns.tex index c8919c307..c89f59dd6 100644 --- a/tutorial/typesfuns.tex +++ b/tutorial/typesfuns.tex @@ -81,7 +81,7 @@ syntax. Natural numbers and lists, for example, can be declared as follows: \begin{SaveVerbatim}{natlist} -data Nat = O | S Nat -- Natural numbers +data Nat = Z | S Nat -- Natural numbers -- (zero and successor) data List a = Nil | (::) a (List a) -- Polymorphic lists @@ -90,7 +90,7 @@ data List a = Nil | (::) a (List a) -- Polymorphic lists \noindent The above declarations are taken from the standard library. Unary natural -numbers can be either zero (\texttt{O} - that's a capital letter 'o', not the digit), or +numbers can be either zero (\texttt{Z}), or the successor of another natural number (\texttt{S k}). Lists can either be empty (\texttt{Nil}) or 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: -- Unary addition plus : Nat -> Nat -> Nat -plus O y = y +plus Z y = y plus (S k) y = S (plus k y) -- Unary multiplication mult : Nat -> Nat -> Nat -mult O y = O +mult Z y = Z mult (S k) y = plus y (mult k y) \end{SaveVerbatim} @@ -148,7 +148,7 @@ The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded for use by \texttt{Nat}, and are implemented using the above functions. Unlike Haskell, there is no restriction on whether types and function names must begin with a capital letter or not. Function -names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S}, +names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{Z}, \tDC{S}, \tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are all part of the same namespace. @@ -156,10 +156,10 @@ We can test these functions at the \Idris{} prompt: \begin{SaveVerbatim}{fntest} -Idris> plus (S (S O)) (S (S O)) -S (S (S (S O))) : Nat -Idris> mult (S (S (S O))) (plus (S (S O)) (S (S O))) -S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat +Idris> plus (S (S Z)) (S (S Z)) +S (S (S (S Z))) : Nat +Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z))) +S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) : Nat \end{SaveVerbatim} \useverb{fntest} @@ -171,9 +171,9 @@ meaning that we can also test the functions as follows: \begin{SaveVerbatim}{fntest} Idris> plus 2 2 -S (S (S (S O))) : Nat +S (S (S (S Z))) : Nat Idris> mult 3 (plus 2 2) -S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat +S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) : Nat \end{SaveVerbatim} \useverb{fntest} @@ -252,13 +252,13 @@ So, for example, the following definitions are legal: \begin{SaveVerbatim}{whereinfer} even : Nat -> Bool -even O = True +even Z = True even (S k) = odd k where - odd O = False + odd Z = False odd (S k) = even k test : List Nat -test = [c (S 1), c O, d (S O)] +test = [c (S 1), c Z, d (S Z)] where c x = 42 + x d y = c (y + 1 + z y) where z w = y + w @@ -278,7 +278,7 @@ we declare vectors as follows: \begin{SaveVerbatim}{vect} data Vect : Type -> Nat -> Type where - Nil : Vect a O + Nil : Vect a Z (::) : a -> Vect a k -> Vect a (S k) \end{SaveVerbatim} @@ -366,12 +366,12 @@ data Fin : Nat -> Type where \useverb{findecl} \noindent -\tDC{fO} is the zeroth element of a finite set with \texttt{S k} elements; +\tDC{fO} is the zeroth element of a finite set with \texttt{S k} elements; \texttt{fS n} is the \texttt{n+1}th element of a finite set with \texttt{S k} elements. \tTC{Fin} is indexed by a \tTC{Nat}, which represents the number of elements in the set. Obviously we can't construct an -element of an empty set, so neither constructor targets \texttt{Fin O}. +element of an empty set, so neither constructor targets \texttt{Fin Z}. A useful application of the \tTC{Fin} family is to represent bounded natural 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 is no larger than the length of the vector. Note also that there is no case for \texttt{Nil} here. This is because it is -impossible. Since there is no element of \texttt{Fin O}, and the location is a -\texttt{Fin n}, then \texttt{n} can not be \tDC{O}. As a result, attempting to +impossible. Since there is no element of \texttt{Fin Z}, and the location is a +\texttt{Fin n}, then \texttt{n} can not be \tDC{Z}. As a result, attempting to look up an element in an empty vector would give a compile time type error, -since it would force \texttt{n} to be \tDC{O}. +since it would force \texttt{n} to be \tDC{Z}. \subsubsection{Implicit Arguments} @@ -520,11 +520,11 @@ data types and functions to be defined simultaneously: mutual even : Nat -> Bool - even O = True + even Z = True even (S k) = odd k odd : Nat -> Bool - odd O = False + odd Z = False odd (S k) = even k \end{SaveVerbatim} @@ -663,7 +663,7 @@ We have already seen the \texttt{List} and \texttt{Vect} data types: data List a = Nil | (::) a (List a) data Vect : Type -> Nat -> Type where - Nil : Vect a O + Nil : Vect a Z (::) : a -> Vect a k -> Vect a (S k) \end{SaveVerbatim} @@ -787,7 +787,7 @@ bounds error: list_lookup : Nat -> List a -> Maybe a list_lookup _ Nil = Nothing -list_lookup O (x :: xs) = Just x +list_lookup Z (x :: xs) = Just x list_lookup (S k) (x :: xs) = list_lookup k xs \end{SaveVerbatim} diff --git a/tutorial/views.tex b/tutorial/views.tex index 564a12180..7fec49634 100644 --- a/tutorial/views.tex +++ b/tutorial/views.tex @@ -10,7 +10,7 @@ determined by whether the vector was empty or not: \begin{SaveVerbatim}{appdep} (++) : Vect a n -> Vect a m -> Vect a (n + m) -(++) {n=O} [] ys = ys +(++) {n=Z} [] ys = ys (++) {n=S k} (x :: xs) ys = x :: xs ++ ys \end{SaveVerbatim} @@ -83,7 +83,7 @@ to write a function which converts a natural number to a list of binary digits \begin{SaveVerbatim}{natToBin} natToBin : Nat -> List Bool -natToBin O = Nil +natToBin Z = Nil natToBin k with (parity k) natToBin (j + j) | even = False :: natToBin j natToBin (S (j + j)) | odd = True :: natToBin j