Agda-2.5.2: A dependently typed functional programming language and proof assistant
Agda.Compiler.JS.Substitution
map :: Nat -> (Nat -> LocalId -> Exp) -> Exp -> Exp #
shift :: Nat -> Exp -> Exp #
shiftFrom :: Nat -> Nat -> Exp -> Exp #
shifter :: Nat -> Nat -> LocalId -> Exp #
subst :: Nat -> [Exp] -> Exp -> Exp #
substituter :: Nat -> [Exp] -> Nat -> LocalId -> Exp #
map' :: Nat -> (Nat -> LocalId -> Exp) -> Exp -> Exp #
subst' :: Nat -> [Exp] -> Exp -> Exp #
apply :: Exp -> [Exp] -> Exp #
lookup :: Exp -> MemberId -> Exp #
self :: Exp -> Exp -> Exp #
fix :: Exp -> Exp #
curriedApply :: Exp -> [Exp] -> Exp #
curriedLambda :: Nat -> Exp -> Exp #
emp :: Exp #
union :: Exp -> Exp -> Exp #
vine :: [MemberId] -> Exp -> Exp #
object :: [([MemberId], Exp)] -> Exp #