@[inline]
Equations
Equations
- Lean.IR.MaxIndex.instAndThenCollector = { andThen := fun a b => Lean.IR.MaxIndex.seq a (b ()) }
Equations
- Lean.IR.MaxIndex.collectDecl x = match x with | Lean.IR.Decl.fdecl x xs x_1 b x_2 => HAndThen.hAndThen (Lean.IR.MaxIndex.collectParams xs) fun x => Lean.IR.MaxIndex.collectFnBody b | Lean.IR.Decl.extern x xs x_1 x_2 => Lean.IR.MaxIndex.collectParams xs
Equations
Equations
@[inline]
Equations
Equations
- Lean.IR.FreeIndices.insertParams s ys = Array.foldl (fun s p => Std.RBTree.insert s p.x.idx) s ys 0 (Array.size ys)
Equations
- Lean.IR.FreeIndices.instAndThenCollector = { andThen := fun a b => Lean.IR.FreeIndices.seq a (b ()) }
Equations
Equations
Equations
- Lean.IR.HasIndex.visitVar w x = (w == x.idx)
Equations
- Lean.IR.HasIndex.visitJP w x = (w == x.idx)
Equations
- Lean.IR.HasIndex.visitArg w x = match x with | Lean.IR.Arg.var x => Lean.IR.HasIndex.visitVar w x | x => false
Equations
- Lean.IR.HasIndex.visitArgs w xs = Array.any xs (Lean.IR.HasIndex.visitArg w) 0 (Array.size xs)
Equations
- Lean.IR.HasIndex.visitParams w ps = Array.any ps (fun p => w == p.x.idx) 0 (Array.size ps)
Equations
- Lean.IR.HasIndex.visitExpr w x = match x with | Lean.IR.Expr.ctor x ys => Lean.IR.HasIndex.visitArgs w ys | Lean.IR.Expr.reset x x_1 => Lean.IR.HasIndex.visitVar w x_1 | Lean.IR.Expr.reuse x x_1 x_2 ys => Lean.IR.HasIndex.visitVar w x || Lean.IR.HasIndex.visitArgs w ys | Lean.IR.Expr.proj x x_1 => Lean.IR.HasIndex.visitVar w x_1 | Lean.IR.Expr.uproj x x_1 => Lean.IR.HasIndex.visitVar w x_1 | Lean.IR.Expr.sproj x x_1 x_2 => Lean.IR.HasIndex.visitVar w x_2 | Lean.IR.Expr.fap x ys => Lean.IR.HasIndex.visitArgs w ys | Lean.IR.Expr.pap x ys => Lean.IR.HasIndex.visitArgs w ys | Lean.IR.Expr.ap x ys => Lean.IR.HasIndex.visitVar w x || Lean.IR.HasIndex.visitArgs w ys | Lean.IR.Expr.box x x_1 => Lean.IR.HasIndex.visitVar w x_1 | Lean.IR.Expr.unbox x => Lean.IR.HasIndex.visitVar w x | Lean.IR.Expr.lit v => false | Lean.IR.Expr.isShared x => Lean.IR.HasIndex.visitVar w x | Lean.IR.Expr.isTaggedPtr x => Lean.IR.HasIndex.visitVar w x
Equations
- Lean.IR.Arg.hasFreeVar arg x = Lean.IR.HasIndex.visitArg x.idx arg
Equations
- Lean.IR.Expr.hasFreeVar e x = Lean.IR.HasIndex.visitExpr x.idx e
Equations
- Lean.IR.FnBody.hasFreeVar b x = Lean.IR.HasIndex.visitFnBody x.idx b