Module

Type.Data.Peano.Nat.Parse

Package: purescript-typelevel-peano
Repository: csicar/purescript-typelevel-peano

#ParseNat Source

class ParseNat (sym :: Symbol) (nat :: Nat) | nat -> sym, sym -> nat

Parses a Nat from a Symbol

ParseNat "2" ~> (Succ (Succ Z))
ParseNat "1283" ~> (Succ (...))

Instances

ParseNat "0" Z
ParseNat "1" (Succ Z)
ParseNat "2" (Succ (Succ Z))
ParseNat "3" (Succ (Succ (Succ Z)))
ParseNat "4" (Succ (Succ (Succ (Succ Z))))
ParseNat "5" (Succ (Succ (Succ (Succ (Succ Z)))))
ParseNat "6" (Succ (Succ (Succ (Succ (Succ (Succ Z))))))
ParseNat "7" (Succ (Succ (Succ (Succ (Succ (Succ (Succ Z)))))))
ParseNat "8" (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Z))))))))
ParseNat "9" (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Z)))))))))
(ParseNat head msd, Cons head tail sym, ProductNat msd D10 high, ParseNat tail lower, SumNat high lower res) => ParseNat sym res

#parseNat Source

parseNat :: forall sym a. ParseNat sym a => SProxy sym -> NProxy a

value-level parse of number

parseNat (SProxy "10") ~> D10

Modules: Type.Data.Peano; Type.Data.Peano.Int; Type.Data.Peano.Int.Definition; Type.Data.Peano.Int.Parse; Type.Data.Peano.Int.TypeAliases; Type.Data.Peano.Nat; Type.Data.Peano.Nat.Definition; Type.Data.Peano.Nat.Parse; Type.Data.Peano.Nat.TypeAliases