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

Data.Eliminator.TypeLits

Description

Crude imitations of eliminator functions for Nat and Symbol.

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
elimSymbol :: forall (p :: Symbol ~> Type) (s :: Symbol). Sing s -> Apply p "" -> (forall (c :: Char) (ss :: Symbol). Sing c -> Sing ss -> Apply p ss -> Apply p (ConsSymbol c ss)) -> Apply p s

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.

elimSymbol :: forall (p :: Symbol ~> Type) (s :: Symbol). Sing s -> Apply p "" -> (forall (c :: Char) (ss :: Symbol). Sing c -> Sing ss -> Apply p ss -> Apply p (ConsSymbol c ss)) -> Apply p s Source #

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