Type.Data.Peano.Nat.Parse

class Length (sym :: Symbol) (nat :: Nat) | sym -> nat

Instances

• Length "" Z
• (Cons head tail sym, Length tail tailLength) => Length sym (Succ tailLength)

length :: forall sproxy proxy a b. Length a b => sproxy a -> proxy b

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, Length tail symLength, ExponentiationNat D10 symLength offset, ProductNat offset msd high, ParseNat tail lower, SumNat high lower res) => ParseNat sym res

parseNat :: forall sproxy proxy sym a. ParseNat sym a => sproxy sym -> proxy a

value-level parse of number

parseNat (Proxy  "10") ~> D10
parseNat (SProxy "10") ~> D10