Copyright	(C) 2017 Ryan Scott
License	BSD-style (see the file LICENSE)
Maintainer	Ryan Scott
Stability	Experimental
Portability	GHC
Safe Haskell	Trustworthy
Language	Haskell2010

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.