Agda.Compiler.JS.Substitution

Documentation

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