Safe Haskell	Safe
Language	Haskell2010

Options.Harg.Het.Proofs

Contents

Description

This module provides type-level functions that need proofs to work properly.

Synopsis

hgcastWith :: forall (a :: k) (b :: k') (r :: Type). (a :~~: b) -> (a ~~ b => r) -> r
type family (xs :: [k]) ++ (ts :: [k]) = (res :: [k]) where ...
class ProofNil xs where
- proofNil :: (xs ++ '[]) :~~: xs
class Proof xs y zs where
- proof :: (xs ++ (y ': zs)) :~~: ((xs ++ '[y]) ++ zs)

Documentation

hgcastWith :: forall (a :: k) (b :: k') (r :: Type). (a :~~: b) -> (a ~~ b => r) -> r Source #

Same as gcastWith but for heterogeneous propositional equality

Concatenation of type-level lists

type family (xs :: [k]) ++ (ts :: [k]) = (res :: [k]) where ... Source #

Append two type-level lists

> :kind! '[Int, Bool] ++ '[Char, Maybe Int]
'[Int, Bool, Char, Maybe Int]

Equations

'[] ++ ys = ys
(x ': xs) ++ ys = x ': (xs ++ ys)

class ProofNil xs where Source #

Proof that appending an empty list to any list has no effect on the latter.

Methods

Instances

ProofNil ([] :: [k]) Source #
Instance details Defined in Options.Harg.Het.Proofs Methods proofNil :: ([] ++ []) :~~: [] Source #
ProofNil xs => ProofNil (x ': xs :: [k]) Source #
Instance details Defined in Options.Harg.Het.Proofs Methods proofNil :: ((x ': xs) ++ []) :~~: (x ': xs) Source #

class Proof xs y zs where Source #

Proof that appending two lists is the same as appending the first element of the second list to the first one, and then appending the rest.

Methods

proof :: (xs ++ (y ': zs)) :~~: ((xs ++ '[y]) ++ zs) Source #

Instances

Proof ([] :: [k]) (y :: k) (zs :: [k]) Source #
Instance details Defined in Options.Harg.Het.Proofs Methods proof :: ([] ++ (y ': zs)) :~~: (([] ++ (y ': [])) ++ zs) Source #
Proof ([] :: [k]) (y :: k) ([] :: [k]) Source #
Instance details Defined in Options.Harg.Het.Proofs Methods proof :: ([] ++ (y ': [])) :~~: (([] ++ (y ': [])) ++ []) Source #
ProofNil (xs ++ (y ': ([] :: [k]))) => Proof (x ': xs :: [k]) (y :: k) ([] :: [k]) Source #
Instance details Defined in Options.Harg.Het.Proofs Methods proof :: ((x ': xs) ++ (y ': [])) :~~: (((x ': xs) ++ (y ': [])) ++ []) Source #
Proof xs y (z ': zs) => Proof (x ': xs :: [a]) (y :: a) (z ': zs :: [a]) Source #	Induction on the tail of the list
Instance details Defined in Options.Harg.Het.Proofs Methods proof :: ((x ': xs) ++ (y ': (z ': zs))) :~~: (((x ': xs) ++ (y ': [])) ++ (z ': zs)) Source #