Language.Symantic.Lib.Function

Symantic for '(->)'.

Class Sym_Function

class Sym_Function term where

Methods

comp :: term (b -> c) -> term (a -> b) -> term (a -> c) infixr 9

const :: term a -> term b -> term a

flip :: term (a -> b -> c) -> term (b -> a -> c)

id :: term a -> term a

comp :: Sym_Function (UnT term) => Trans term => term (b -> c) -> term (a -> b) -> term (a -> c) infixr 9

const :: Sym_Function (UnT term) => Trans term => term a -> term b -> term a

flip :: Sym_Function (UnT term) => Trans term => term (a -> b -> c) -> term (b -> a -> c)

id :: Sym_Function (UnT term) => Trans term => term a -> term a

Instances

Sym_Function View

Defined in Language.Symantic.Lib.Function

Methods

comp :: View (b -> c) -> View (a -> b) -> View (a -> c)

const :: View a -> View b -> View a

flip :: View (a -> b -> c) -> View (b -> a -> c)

id :: View a -> View a

Sym_Function Eval

Defined in Language.Symantic.Lib.Function

Methods

comp :: Eval (b -> c) -> Eval (a -> b) -> Eval (a -> c)

const :: Eval a -> Eval b -> Eval a

flip :: Eval (a -> b -> c) -> Eval (b -> a -> c)

id :: Eval a -> Eval a

(Sym_Function term, Sym_Lambda term) => Sym_Function (BetaT term)

Defined in Language.Symantic.Lib.Function

Methods

comp :: BetaT term (b -> c) -> BetaT term (a -> b) -> BetaT term (a -> c)

const :: BetaT term a -> BetaT term b -> BetaT term a

flip :: BetaT term (a -> b -> c) -> BetaT term (b -> a -> c)

id :: BetaT term a -> BetaT term a

(Sym_Function r1, Sym_Function r2) => Sym_Function (Dup r1 r2)

Defined in Language.Symantic.Lib.Function

Methods

comp :: Dup r1 r2 (b -> c) -> Dup r1 r2 (a -> b) -> Dup r1 r2 (a -> c)

const :: Dup r1 r2 a -> Dup r1 r2 b -> Dup r1 r2 a

flip :: Dup r1 r2 (a -> b -> c) -> Dup r1 r2 (b -> a -> c)

id :: Dup r1 r2 a -> Dup r1 r2 a

Types

tyFun :: Source src => LenInj vs => Type src vs (->)

a0 :: Source src => LenInj vs => KindInj (K a) => Type src (Proxy a ': vs) a

b1 :: Source src => LenInj vs => KindInj (K b) => Type src (a ': (Proxy b ': vs)) b

c2 :: Source src => LenInj vs => KindInj (K c) => Type src (a ': (b ': (Proxy c ': vs))) c

Terms

teFunction_compose :: TermDef (->) '[Proxy a, Proxy b, Proxy c] (() #> ((b -> c) -> (a -> b) -> a -> c))

teFunction_const :: TermDef (->) '[Proxy a, Proxy b] (() #> (a -> b -> a))

teFunction_flip :: TermDef (->) '[Proxy a, Proxy b, Proxy c] (() #> ((a -> b -> c) -> b -> a -> c))

teFunction_id :: TermDef (->) '[Proxy a] (() #> (a -> a))

teFunction_apply :: TermDef (->) '[Proxy a, Proxy b] (() #> ((a -> b) -> a -> b))

Orphan instances

Gram_Term_AtomsFor src ss g ((->) :: * -> * -> *)

Methods

g_term_atomsFor :: [CF g (AST_Term src ss)]

(Source src, SymInj ss ((->) :: * -> * -> *)) => ModuleFor src ss ((->) :: * -> * -> *)

Methods

moduleFor :: (PathMod, Module src ss)

ClassInstancesFor ((->) :: * -> * -> *)

Methods

proveConstraintFor :: Source src => proxy (->) -> Type src vs q -> Maybe (Qual q)

TypeInstancesFor ((->) :: * -> * -> *)

Methods

expandFamFor :: Source src => proxy (->) -> Len vs -> Const src fam -> Types src vs ts -> Maybe (Type src vs (Fam fam ts))

NameTyOf ((->) :: * -> * -> *)

Methods

nameTyOf :: proxy (->) -> Mod NameTy

isNameTyOp :: proxy (->) -> Bool