h*9K5@      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ 0.2.0.0 Safe-Inferred *16dnatural-arithmetic>Proof that the first argument is equal to the second argument.natural-arithmeticProof that the first argument is less than or equal to the second argument. natural-arithmeticProof that the first argument is strictly less than the second argument. natural-arithmetic Variant of " that only allows 32-bit integers.natural-arithmetic Either a Fin# or Nothing. Internally, this uses negative one to mean Nothing.natural-arithmetic?Finite numbers without the overhead of carrying around a proof.natural-arithmeticUnboxed variant of Nat.natural-arithmetic1A value-level representation of a natural number n.      44444 4 Safe-Inferred()*1natural-arithmeticProof that the first argument can be expressed as the sum of the second argument and some other natural number.natural-arithmeticA finite set of n# elements. 'Fin n = { 0 .. n - 1 }' ! #"  ! #"  Safe-Inferred1 ''natural-arithmetic5Any number plus zero is equal to the original number.(natural-arithmetic5Zero plus any number is equal to the original number.)natural-arithmeticAddition is commutative.*natural-arithmeticAddition is associative.(')*(')* Safe-Inferred 1P=natural-arithmeticInfix synonym of A.>natural-arithmeticInfix synonym of C.?natural-arithmeticInfix synonym of D.Anatural-arithmetic>Is the first argument strictly less than the second argument?Cnatural-arithmeticIs the first argument less-than-or-equal-to the second argument?Dnatural-arithmetic+Are the two arguments equal to one another?Fnatural-arithmetic-Is zero equal to this number or less than it?Hnatural-arithmeticAdd two numbers.Inatural-arithmetic Variant of H for unboxed nats.Jnatural-arithmetic.Divide two numbers. Rounds down (towards zero)Knatural-arithmetic.Divide two numbers. Rounds up (away from zero)Lnatural-arithmeticMultiply two numbers.Mnatural-arithmeticThe successor of a number.Nnatural-arithmeticUnlifted variant of M.Onatural-arithmetic5Subtract the second argument from the first argument.Pnatural-arithmeticThe number zero.Qnatural-arithmeticThe number one.Rnatural-arithmeticThe number two.Snatural-arithmeticThe number three.Tnatural-arithmeticUse GHC's built-in type-level arithmetic to create a witness of a type-level number. This only reduces if the number is a constant.Vnatural-arithmeticThe number zero. Unboxed.Wnatural-arithmeticThe number one. Unboxed.Xnatural-arithmetic Extract the  from a . This is intended to be used at a boundary where a safe interface meets the unsafe primitives on top of which it is built.Znatural-arithmeticRun a computation on a witness of a type-level number. The argument  must be greater than or equal to zero. This is not checked. Failure to upload this invariant will lead to a segfault.3HIOJKLMNDEABCFG?=@>PQRSTUVW<;:9876543210/.-,+XY\]Z[3HIOJKLMNDEABCFG?=@>PQRSTUVW<;:9876543210/.-,+XY\]Z[ Safe-Inferred 1^natural-arithmeticReplace the left-hand side of a strict inequality with an equal number._natural-arithmeticReplace the right-hand side of a strict inequality with an equal number.`natural-arithmeticAdd two inequalities.bnatural-arithmetic,Compose two inequalities using transitivity.dnatural-arithmetic+Any number is less-than-or-equal-to itself.fnatural-arithmeticAdd a constant to the left-hand side of both sides of the inequality.hnatural-arithmeticAdd a constant to the right-hand side of both sides of the inequality.jnatural-arithmeticAdd a constant to the left-hand side of the right-hand side of the inequality.lnatural-arithmeticAdd a constant to the right-hand side of the right-hand side of the inequality.nnatural-arithmeticSubtract a constant from the left-hand side of both sides of the inequality. This is the opposite of f.pnatural-arithmeticSubtract a constant from the right-hand side of both sides of the inequality. This is the opposite of h.rnatural-arithmetic6Weaken a strict inequality to a non-strict inequality.tnatural-arithmeticWeaken a strict inequality to a non-strict inequality, incrementing the right-hand argument by one.vnatural-arithmetic)Zero is less-than-or-equal-to any number.wnatural-arithmeticUse GHC's built-in type-level arithmetic to prove that one number is less-than-or-equal-to another. The type-checker only reduces ! if both arguments are constants.vde^_fghinopqjklmbc`arstuwyxvde^_fghinopqjklmbc`arstuwyx Safe-Inferred 1|natural-arithmeticReplace the left-hand side of a strict inequality with an equal number.}natural-arithmeticReplace the right-hand side of a strict inequality with an equal number.~natural-arithmetic2Add a strict inequality to a nonstrict inequality.natural-arithmeticAdd a constant to the left-hand side of both sides of the strict inequality.natural-arithmeticAdd a constant to the right-hand side of both sides of the strict inequality.natural-arithmeticSubtract a constant from the left-hand side of both sides of the inequality. This is the opposite of .natural-arithmeticSubtract a constant from the right-hand side of both sides of the inequality. This is the opposite of .natural-arithmeticAdd a constant to the left-hand side of the right-hand side of the strict inequality.natural-arithmeticAdd a constant to the right-hand side of the right-hand side of the strict inequality.natural-arithmetic3Compose two strict inequalities using transitivity.natural-arithmeticCompose a strict inequality (the first argument) with a nonstrict inequality (the second argument).natural-arithmeticZero is less than one.natural-arithmeticNothing is less than zero.natural-arithmeticUse GHC's built-in type-level arithmetic to prove that one number is less than another. The type-checker only reduces ! if both arguments are constants.natural-arithmetic Given that m < n/p, we know that p*m < n.natural-arithmetic Given that m < roundUp(n/p), we know that p*m < n.#|}~{z#|}~{z Safe-Inferred1s Safe-Inferred)*14natural-arithmeticRaise the index by m and weaken the bound by m , adding m to the right-hand side of n.natural-arithmeticRaise the index by m and weaken the bound by m , adding m to the left-hand side of n.natural-arithmeticWeaken the bound by m, adding it to the left-hand side of the existing bound. This does not change the index.natural-arithmeticWeaken the bound by m, adding it to the right-hand side of the existing bound. This does not change the index.natural-arithmeticWeaken the bound, replacing it by another number greater than or equal to itself. This does not change the index.natural-arithmetic(A finite set of no values is impossible.natural-arithmetic!Fold over the numbers bounded by n in descending order. This is lazy in the accumulator. For convenince, this differs from foldr in the order of the parameters. 'descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))natural-arithmetic!Fold over the numbers bounded by n in descending order. This is strict in the accumulator. For convenince, this differs from foldr' in the order of the parameters. 'descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))natural-arithmetic!Fold over the numbers bounded by n6 in ascending order. This is lazy in the accumulator. &ascend 4 z f = f 3 (f 2 (f 1 (f 0 z)))natural-arithmetic(Strict fold over the numbers bounded by n8 in ascending order. For convenince, this differs from foldl'! in the order of the parameters. 'ascend' 4 z f = f 3 (f 2 (f 1 (f 0 z)))natural-arithmeticGeneralization of ascend'. that lets the caller pick the starting index: ascend' === ascendFrom' 0natural-arithmetic Variant of  ascendFrom' with unboxed arguments.natural-arithmetic5Strict monadic left fold over the numbers bounded by n in ascending order. Roughly: ascendM 4 z0 f = f 0 z0 >>= \z1 -> f 1 z1 >>= \z2 -> f 2 z2 >>= \z3 -> f 3 z3natural-arithmetic Variant of ascendM that takes an unboxed Nat and provides an unboxed Fin to the callback.natural-arithmetic,Monadic traversal of the numbers bounded by n in ascending order. 'ascendM_ 4 f = f 0 *> f 1 *> f 2 *> f 3natural-arithmetic Variant of ascendM_ that takes an unboxed Nat and provides an unboxed Fin to the callback.natural-arithmetic5Strict monadic left fold over the numbers bounded by n in descending order. Roughly: descendM 4 z f = f 3 z0 >>= \z1 -> f 2 z1 >>= \z2 -> f 1 z2 >>= \z3 -> f 0 z3natural-arithmetic,Monadic traversal of the numbers bounded by n in descending order. (descendM_ 4 f = f 3 *> f 2 *> f 1 *> f 0natural-arithmetic7Generate all values of a finite set in ascending order.ascending (Nat.constant @3)[Fin 0,Fin 1,Fin 2]natural-arithmetic8Generate all values of a finite set in descending order.descending (Nat.constant @3)[Fin 2,Fin 1,Fin 0]natural-arithmetic Generate len values starting from off in ascending order.ascendingSlice (Nat.constant @2) (Nat.constant @3) (Lte.constant @_ @6)[Fin 2,Fin 3,Fin 4]natural-arithmetic Generate len: values starting from 'off + len - 1' in descending order.descendingSlice (Nat.constant @2) (Nat.constant @3) (Lt.constant @6)[Fin 4,Fin 3,Fin 2]natural-arithmetic Extract the  from a 'Fin n'. This is intended to be used at a boundary where a safe interface meets the unsafe primitives on top of which it is built.natural-arithmetic4Consume the natural number and the proof in the Fin.natural-arithmetic Variant of ' for unboxed argument and result types.natural-arithmeticReturn the successor of the Fin or return nothing if the argument is the greatest inhabitant.natural-arithmetic Variant of  for unlifted finite numbers.natural-arithmeticThis crashes if n = 0 . Divides i by n and takes the remainder.natural-arithmeticThis crashes if n = 0 . Divides i by n and takes the remainder. natural-arithmetic Upper boundnatural-arithmeticInitial accumulatornatural-arithmeticUpdate accumulatornatural-arithmetic Upper boundnatural-arithmeticInitial accumulatornatural-arithmeticUpdate accumulatornatural-arithmetic Upper boundnatural-arithmeticInitial accumulatornatural-arithmeticUpdate accumulatornatural-arithmetic Upper boundnatural-arithmeticInitial accumulatornatural-arithmeticUpdate accumulatornatural-arithmeticIndex to start atnatural-arithmeticNumber of steps to takenatural-arithmeticInitial accumulatornatural-arithmeticUpdate accumulatornatural-arithmeticIndex to start atnatural-arithmeticNumber of steps to takenatural-arithmeticInitial accumulatornatural-arithmeticUpdate accumulatornatural-arithmetic Upper boundnatural-arithmeticInitial accumulatornatural-arithmeticUpdate accumulatornatural-arithmetic Upper boundnatural-arithmeticInitial accumulatornatural-arithmeticUpdate accumulatornatural-arithmetic Upper boundnatural-arithmeticEffectful interpretionnatural-arithmetic Upper boundnatural-arithmeticUpdate accumulatornatural-arithmetic Upper boundnatural-arithmeticEffectful interpretion##      !"##$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`aJKbcdefghijklmnopqrstuRV^_vw`aJKfghinopqjkxylmbcz{|}RX~VW^__hifjl~Z[_^\]OP1natural-arithmetic-0.2.0.0-3w4mdLkA7S2L7UvkdhJOEkArithmetic.UnsafeArithmetic.TypesArithmetic.PlusArithmetic.NatArithmetic.Lte Arithmetic.LtArithmetic.EqualArithmetic.Finnatural-arithmetic:=:#Eq#:=:Eq<=#Lte#<=Lte<#Lt#<LtFin32# MaybeFin#Fin#Nat#NatgetNat$fCategoryNatural<=$fCategoryNatural:=: $fShowNat DifferenceFinindexproofWithNatMaybeFinNothing# MaybeFinJust#$fOrdFin$fEqFin $fShowFinzeroRzeroL commutative associativeN4096#N2048#N1024#N512#N256#N128#N64#N32#N16#N8#N7#N6#N5#N4#N3#N2#N1#N0#