initSidebarItems({"struct":[["Pred","For any non-positive Peano number `N`, we define its predecessor, `Pred<N>`."],["Succ","For any non-negative Peano number `N`, we define its successor, `Succ<N>`."],["Zero","The type corresponding to the Peano number 0."]],"trait":[["NonNeg","Implemented for `Zero` and all numbers of the form `Succ<N: NonNeg>`."],["NonPos","Implemented for `Zero` and all numbers of the form `Pred<N: NonPos>`."],["NonZero","Implemented for all Peano numbers of the form `Succ<M: NonNeg>` or `Pred<N: NonPos>`."],["Peano","All numbers defined in this module belong to the **Peano** trait. It should not be implemented for anything else."],["Same","`Same` is used to ensure that two types are the same. Its `Output` should **always** be that type."],["ToInt","Convert a Peano number to the integer it represents."]],"type":[["N1","The Peano number -1; `N1 = Pred<Zero>;`"],["N2","The Peano number -2; `N2 = Pred<N1>;`"],["N3","The Peano number -3; `N3 = Pred<N2>;`"],["N4","The Peano number -4; `N4 = Pred<N3>;`"],["N5","The Peano number -5; `N5 = Pred<N4>;`"],["N6","The Peano number -6; `N6 = Pred<N5>;`"],["N7","The Peano number -7; `N7 = Pred<N6>;`"],["N8","The Peano number -8; `N8 = Pred<N7>;`"],["N9","The Peano number -9; `N9 = Pred<N8>;`"],["P1","The Peano number +1; `P1 = Succ<Zero>;`"],["P2","The Peano number +2; `P2 = Succ<P1>;`"],["P3","The Peano number +3; `P3 = Succ<P2>;`"],["P4","The Peano number +4; `P4 = Succ<P3>;`"],["P5","The Peano number +5; `P5 = Succ<P4>;`"],["P6","The Peano number +6; `P6 = Succ<P5>;`"],["P7","The Peano number +7; `P7 = Succ<P6>;`"],["P8","The Peano number +8; `P8 = Succ<P7>;`"],["P9","The Peano number +9; `P9 = Succ<P8>;`"]]});