ModuleAgda-2.8.0.2Haskell2010

Agda.Compiler.JS.Substitution

Synopsis

valuemap :: Nat -> (Nat -> LocalId -> Exp) -> Exp -> Exp

valueshift :: Nat -> Exp -> Exp

valueshiftFrom :: Nat -> Nat -> Exp -> Exp

valueshifter :: Nat -> Nat -> LocalId -> Exp

valuesubst :: Nat -> [Exp] -> Exp -> Exp

valuesubstituter :: Nat -> [Exp] -> Nat -> LocalId -> Exp

valuesubstShift :: Nat -> Nat -> [Exp] -> Exp -> Exp

valuemap' :: Nat -> (Nat -> LocalId -> Exp) -> Exp -> Exp

valuesubst' :: Nat -> [Exp] -> Exp -> Exp

valueapply :: Exp -> [Exp] -> Exp

valuelookup :: Exp -> MemberId -> Exp

valueself :: Exp -> Exp -> Exp

valuefix :: Exp -> Exp

valuecurriedApply :: Exp -> [Exp] -> Exp

valuecurriedLambda :: Nat -> Exp -> Exp

valueemp :: Exp

valueunion :: Exp -> Exp -> Exp

valuevine :: [MemberId] -> Exp -> Exp

valueobject :: [([MemberId], Exp)] -> Exp