Language.Symantic.Compiling.Term

Type Term

data Term src ss ts vs t

typeOfTerm

Type TermT

data TermT src ss ts vs

Type TermVT

data TermVT src ss ts

liftTermVT

Type TermAVT

data TermAVT src ss

Type TeSym

data TeSym ss ts t

teSym

Type family QualOf

type family QualOf (t :: Type) :: Constraint where ...

Type family UnQualOf

type family UnQualOf (t :: Type) :: Type where ...

unQualTy

unQualsTy

Type CtxTe

data CtxTe term hs

Type TermDef

type TermDef s vs t

Type family Sym

type family Sym (s :: Type) :: (Type -> Type) -> Constraint

Type family Syms

type family Syms (ss :: [Type]) (term :: Type -> Type) :: Constraint where ...

Type Inj_Sym

type Inj_Sym ss s

inj_Sym

Class Inj_SymP

class Inj_SymP p ss s

Class Sym_Lambda

class Sym_Lambda term

lam2

lam3

lam4