Module

Type.Data.Peano.Nat.Parse

#Length

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

Instances

#length

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

#ParseNat

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

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

Modules