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

Safe HaskellNone
LanguageHaskell98

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

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