Agda-2.6.4: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Compiler.JS.Substitution

Documentation

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

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

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

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

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

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

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

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

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