search

nfrisby / frags

Plugin gonna getcha, row types
0 stars 1 forks source link

type families witnessing injection from Nat into Frag () #40

Open nfrisby opened 5 years ago

nfrisby commented 5 years ago 
type family FragNat (fr :: Frag ()) :: Nat where
  FragNat 'Nil = 0

type family NatFrag (z :: Nat) :: Frag () where
  NatFrag 0 = 'Nil
  NatFrag n = NatFrag (n - 1) :+ '()

The plugin should at least reduce NatFrag (FragNat fr) to fr and FragNat (NatFrag n) to n.