eliminators-0.4.1: Dependently typed elimination functions using singletons

Data.Eliminator.TypeNats

Description

A crude imitation of an eliminator function for Nat.

Synopsis

# Documentation

elimNat :: forall (p :: Nat ~> Type) (n :: Nat). Sing n -> (p @@ 0) -> (forall (k :: Nat). Sing k -> (p @@ k) -> p @@ (k + 1)) -> p @@ n Source #

Although Nat is not actually an inductive data type in GHC, we can (crudely) pretend that it is using this eliminator.