Language.Symantic.Lib.List

Symantic for '[]'.

Class Sym_List

class Sym_List term where

Methods

list_empty :: term [a]

list_cons :: term a -> term [a] -> term [a] infixr 5

list :: [term a] -> term [a]

zipWith :: term (a -> b -> c) -> term [a] -> term [b] -> term [c]

list_empty :: Sym_List (UnT term) => Trans term => term [a]

list_cons :: Sym_List (UnT term) => Trans term => term a -> term [a] -> term [a] infixr 5

list :: Sym_List (UnT term) => Trans term => [term a] -> term [a]

zipWith :: Sym_List (UnT term) => Trans term => term (a -> b -> c) -> term [a] -> term [b] -> term [c]

Instances

Sym_List Eval

Methods

list_empty :: Eval [a]

list_cons :: Eval a -> Eval [a] -> Eval [a]

list :: [Eval a] -> Eval [a]

zipWith :: Eval (a -> b -> c) -> Eval [a] -> Eval [b] -> Eval [c]

Sym_List View

Methods

list_empty :: View [a]

list_cons :: View a -> View [a] -> View [a]

list :: [View a] -> View [a]

zipWith :: View (a -> b -> c) -> View [a] -> View [b] -> View [c]

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

Methods

list_empty :: BetaT term [a]

list_cons :: BetaT term a -> BetaT term [a] -> BetaT term [a]

list :: [BetaT term a] -> BetaT term [a]

zipWith :: BetaT term (a -> b -> c) -> BetaT term [a] -> BetaT term [b] -> BetaT term [c]

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

Methods

list_empty :: Dup r1 r2 [a]

list_cons :: Dup r1 r2 a -> Dup r1 r2 [a] -> Dup r1 r2 [a]

list :: [Dup r1 r2 a] -> Dup r1 r2 [a]

zipWith :: Dup r1 r2 (a -> b -> c) -> Dup r1 r2 [a] -> Dup r1 r2 [b] -> Dup r1 r2 [c]

Types

tyList :: Source src => LenInj vs => Type src vs a -> Type src vs [a]

Terms

teList_empty :: Source src => SymInj ss [] => Term src ss ts '[Proxy a] (() #> [a])

teList_cons :: Source src => SymInj ss [] => Term src ss ts '[Proxy a] (() #> (a -> [a] -> [a]))

teList_zipWith :: Source src => SymInj ss [] => Term src ss ts '[Proxy a, Proxy b, Proxy c] (() #> ((a -> b -> c) -> [a] -> [b] -> [c]))

Orphan instances

ClassInstancesFor (* -> *) []

Methods

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

TypeInstancesFor (* -> *) []

Methods

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

NameTyOf (* -> *) []

Methods

nameTyOf :: proxy c -> Mod NameTy

isNameTyOp :: proxy c -> Bool

FixityOf (* -> *) []

Methods

fixityOf :: proxy c -> Maybe Fixity

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

Methods

moduleFor :: (PathMod, Module ss [])

(Gram_App g, Gram_Rule g, Gram_Comment g, Gram_Term src ss g, SymInj (* -> *) ss []) => Gram_Term_AtomsFor (* -> *) src ss g []

Methods

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