úÎ#ß ±<      !"#$%&'()*+,-./0123456789:;Singletons for GHC TypeLits(C) 2017 mniipMITmniip@mniip.com experimentalportableNone %&+,-/DOQRT 'A positive number is either a digit in [1, b)#, or another positive number times b plus a digit in [0, b).LA positive number is either 1, or twice another positive number plus 0 or 1.HA positive number is either 1 or a successor of another positive number. 6A class of singletons capable of representing postive < natural numbers. !A natural number is either 0, or b. times another natural number plus a digit in [1, b].JA natural number is either 0, or twice another natural number plus 1 or 2.FA natural number is either 0 or a successor of another natural number.1A natural number is either 0 or 1 plus something.!Auxiliary class for implementing = on higher-kinded singletons.2A class of singletons capable of representing any < natural number.0  !"#$%&'()*+,-./        !"#$%&'()*+,-./Induction for GHC TypeLits(C) 2017 mniipMITmniip@mniip.com experimentalportableNone %&+,-/DOQRT58(\forall n. n > 0 \to P(n)) \to P(0) \to \forall m. P(m)6;(\forall n. P(n) \to P(n + 1)) \to P(0) \to \forall m. P(m)7i(\forall n. P(n) \to P(2n + 1)) \to \\ (\forall n. P(n) \to P(2n + 2)) \to \\ P(0) \to \\ \forall m. P(m)8y\forall b. (\prod_d Q(d)) \to \\ (\forall n. \forall d. d < b \to Q(d) \to P(n) \to P(bn + d + 1)) \to \\ \forall m. P(m)9?(\forall n. P(n) \to P(n + 1)) \to P(1) \to \forall m > 0. P(m):i(\forall n. P(n) \to P(2n)) \to \\ (\forall n. P(n) \to P(2n + 1)) \to \\ P(1) \to \\ \forall m > 0. P(m);°\forall b. (\prod_d Q(d)) \to \\ (\forall n. \forall d. d < b \to Q(d) \to P(n) \to P(bn + d)) \to \\ (\forall d. d > 0 \to d < b \to Q(d) \to P(d)) \to \\ \forall m > 0. P (m)56789:;56789:;56789:;56789:;>      !"#$%&'()*+,-./0123456789:;<=>?@A?BCD1singleton-typelits-0.0.0.0-7IatIBZTaPQ5oqwkhRCCEUGHC.TypeLits.SingletonsGHC.TypeLits.InductionPosBaseBaseLead BaseDigit PosBinaryBinOneBin0Bin1UnaryUnaryOne UnarySuccPositiveSingleton posSingleton NatBaseComp BaseCompZero BaseCompxBp1p NatTwosComp TwosCompZero TwosCompx2p1 TwosCompx2p2NatPeano PeanoZero PeanoSucc NatIsZeroIsZero IsNonZeroShowN showsPrecN NatSingleton natSingleton$fPositiveSingletonPosBase$fShowNPosBase $fShowPosBase$fPositiveSingletonPosBinary$fShowNPosBinary$fPositiveSingletonUnary $fShowNUnary$fPositiveSingletonProxy$fNatSingletonNatBaseComp$fShowNNatBaseComp$fShowNatBaseComp$fNatSingletonNatTwosComp$fShowNNatTwosComp$fNatSingletonNatPeano$fShowNNatPeano$fNatSingletonNatIsZero$fShowNNatIsZero$fNatSingletonProxy $fShowNProxy$fShowPosBinary $fShowUnary$fShowNatTwosComp$fShowNatPeano$fShowNatIsZero induceIsZero inducePeanoinduceTwosCompinduceBaseComp induceUnaryinducePosBinary inducePosBasebase GHC.TypeLitsKnownNatGHC.ShowShow