@[reducible, inline]
Equations
Instances For
Equations
Instances For
Return true if variable, parameter and join point ids are unique
Instances For
@[reducible, inline]
Instances For
Equations
Instances For
Equations
- Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.ctor c ys) x✝ = Lean.IR.Expr.ctor c (Lean.IR.NormalizeIds.normArgs ys x✝)
- Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.reset n x_2) x✝ = Lean.IR.Expr.reset n (Lean.IR.NormalizeIds.normVar x_2 x✝)
- Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.reuse x_2 c u ys) x✝ = Lean.IR.Expr.reuse (Lean.IR.NormalizeIds.normVar x_2 x✝) c u (Lean.IR.NormalizeIds.normArgs ys x✝)
- Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.proj i x_2) x✝ = Lean.IR.Expr.proj i (Lean.IR.NormalizeIds.normVar x_2 x✝)
- Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.uproj i x_2) x✝ = Lean.IR.Expr.uproj i (Lean.IR.NormalizeIds.normVar x_2 x✝)
- Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.sproj n o x_2) x✝ = Lean.IR.Expr.sproj n o (Lean.IR.NormalizeIds.normVar x_2 x✝)
- Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.fap c ys) x✝ = Lean.IR.Expr.fap c (Lean.IR.NormalizeIds.normArgs ys x✝)
- Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.pap c ys) x✝ = Lean.IR.Expr.pap c (Lean.IR.NormalizeIds.normArgs ys x✝)
- Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.ap x_2 ys) x✝ = Lean.IR.Expr.ap (Lean.IR.NormalizeIds.normVar x_2 x✝) (Lean.IR.NormalizeIds.normArgs ys x✝)
- Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.box t x_2) x✝ = Lean.IR.Expr.box t (Lean.IR.NormalizeIds.normVar x_2 x✝)
- Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.unbox x_2) x✝ = Lean.IR.Expr.unbox (Lean.IR.NormalizeIds.normVar x_2 x✝)
- Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.isShared x_2) x✝ = Lean.IR.Expr.isShared (Lean.IR.NormalizeIds.normVar x_2 x✝)
- Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.lit v) x✝ = Lean.IR.Expr.lit v
Instances For
@[reducible, inline]
Equations
Instances For
@[inline]
Equations
- Lean.IR.NormalizeIds.withVar x k m = do let n ← getModify fun (n : Nat) => n + 1 k { idx := n } (Lean.RBMap.insert m x.idx n)
Instances For
@[inline]
Equations
- Lean.IR.NormalizeIds.withJP x k m = do let n ← getModify fun (n : Nat) => n + 1 k { idx := n } (Lean.RBMap.insert m x.idx n)
Instances For
Equations
- Lean.IR.NormalizeIds.instMonadLiftMN = { monadLift := fun {α : Type} (x : Lean.IR.NormalizeIds.M α) (m : Lean.IR.IndexRenaming) => pure (x m) }
Equations
- One or more equations did not get rendered due to their size.
- Lean.IR.NormalizeIds.normDecl d = pure d
Instances For
Create a declaration equivalent to d
s.t. d.normalizeIds.uniqueIds == true
Instances For
Apply a function f : VarId → VarId
to variable occurrences.
The following functions assume the IR code does not have variable shadowing.
Instances For
Equations
- Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.ctor c ys) = Lean.IR.Expr.ctor c (Lean.IR.MapVars.mapArgs f ys)
- Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.reset n x_1) = Lean.IR.Expr.reset n (f x_1)
- Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.reuse x_1 c u ys) = Lean.IR.Expr.reuse (f x_1) c u (Lean.IR.MapVars.mapArgs f ys)
- Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.proj i x_1) = Lean.IR.Expr.proj i (f x_1)
- Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.uproj i x_1) = Lean.IR.Expr.uproj i (f x_1)
- Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.sproj n o x_1) = Lean.IR.Expr.sproj n o (f x_1)
- Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.fap c ys) = Lean.IR.Expr.fap c (Lean.IR.MapVars.mapArgs f ys)
- Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.pap c ys) = Lean.IR.Expr.pap c (Lean.IR.MapVars.mapArgs f ys)
- Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.ap x_1 ys) = Lean.IR.Expr.ap (f x_1) (Lean.IR.MapVars.mapArgs f ys)
- Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.box t x_1) = Lean.IR.Expr.box t (f x_1)
- Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.unbox x_1) = Lean.IR.Expr.unbox (f x_1)
- Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.isShared x_1) = Lean.IR.Expr.isShared (f x_1)
- Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.lit v) = Lean.IR.Expr.lit v
Instances For
@[inline]
Instances For
Replace x
with y
in b
. This function assumes b
does not shadow x