@[reducible, inline]

abbrev Lean.IR.UniqueIds.M (α : Type) : Type

def Lean.IR.UniqueIds.checkId (id : Index) : M Bool

def Lean.IR.UniqueIds.checkParams (ps : Array Param) : M Bool

partial def Lean.IR.UniqueIds.checkFnBody : FnBody → M Bool

def Lean.IR.UniqueIds.checkDecl : Decl → M Bool

def Lean.IR.Decl.uniqueIds (d : Decl) : Bool

Return true if variable, parameter and join point ids are unique

@[reducible, inline]

abbrev Lean.IR.NormalizeIds.M (α : Type) : Type

def Lean.IR.NormalizeIds.normIndex (x : Index) : M Index

def Lean.IR.NormalizeIds.normVar (x : VarId) : M VarId

def Lean.IR.NormalizeIds.normJP (x : JoinPointId) : M JoinPointId

def Lean.IR.NormalizeIds.normArg : Arg → M Arg

def Lean.IR.NormalizeIds.normArgs (as : Array Arg) : M (Array Arg)

def Lean.IR.NormalizeIds.normExpr : Expr → M Expr

@[reducible, inline]

abbrev Lean.IR.NormalizeIds.N (α : Type) : Type

@[inline]

def Lean.IR.NormalizeIds.withVar {α : Type} (x : VarId) (k : VarId → N α) : N α

@[inline]

def Lean.IR.NormalizeIds.withJP {α : Type} (x : JoinPointId) (k : JoinPointId → N α) : N α

@[inline]

def Lean.IR.NormalizeIds.withParams {α : Type} (ps : Array Param) (k : Array Param → N α) : N α

instance Lean.IR.NormalizeIds.instMonadLiftMN : MonadLift M N

partial def Lean.IR.NormalizeIds.normFnBody : FnBody → N FnBody

def Lean.IR.NormalizeIds.normDecl (d : Decl) : N Decl

def Lean.IR.Decl.normalizeIds (d : Decl) : Decl

Create a declaration equivalent to d s.t. d.normalizeIds.uniqueIds == true

Apply a function f : VarId → VarId to variable occurrences. The following functions assume the IR code does not have variable shadowing.

@[inline]

def Lean.IR.MapVars.mapArg (f : VarId → VarId) : Arg → Arg

def Lean.IR.MapVars.mapArgs (f : VarId → VarId) (as : Array Arg) : Array Arg

def Lean.IR.MapVars.mapExpr (f : VarId → VarId) : Expr → Expr

partial def Lean.IR.MapVars.mapFnBody (f : VarId → VarId) : FnBody → FnBody

@[inline]

def Lean.IR.FnBody.mapVars (f : VarId → VarId) (b : FnBody) : FnBody

def Lean.IR.FnBody.replaceVar (x y : VarId) (b : FnBody) : FnBody

Replace x with y in b. This function assumes b does not shadow x