Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Compiler.JS.Substitution

# Documentation

map :: Nat -> (Nat -> LocalId -> Exp) -> Exp -> Exp Source #

shift :: Nat -> Exp -> Exp Source #

shiftFrom :: Nat -> Nat -> Exp -> Exp Source #

shifter :: Nat -> Nat -> LocalId -> Exp Source #

subst :: Nat -> [Exp] -> Exp -> Exp Source #

substituter :: Nat -> [Exp] -> Nat -> LocalId -> Exp Source #

substShift :: Nat -> Nat -> [Exp] -> Exp -> Exp Source #

map' :: Nat -> (Nat -> LocalId -> Exp) -> Exp -> Exp Source #

subst' :: Nat -> [Exp] -> Exp -> Exp Source #

apply :: Exp -> [Exp] -> Exp Source #

lookup :: Exp -> MemberId -> Exp Source #

self :: Exp -> Exp -> Exp Source #

fix :: Exp -> Exp Source #

curriedApply :: Exp -> [Exp] -> Exp Source #

curriedLambda :: Nat -> Exp -> Exp Source #

emp :: Exp Source #

union :: Exp -> Exp -> Exp Source #

vine :: [MemberId] -> Exp -> Exp Source #

object :: [([MemberId], Exp)] -> Exp Source #