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

Data.Eliminator.TypeNats

Description

A crude imitation of an eliminator function for Nat.

Synopsis

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

Documentation

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

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