structure Lean.Compiler.atMostOnce.AtMostOnceData : Type

• found : Bool
• result : Bool

def Lean.Compiler.atMostOnce.Visitor : Type

@[inline]

def Lean.Compiler.atMostOnce.seq (f : Lean.Compiler.atMostOnce.Visitor) (g : Lean.Compiler.atMostOnce.Visitor) : Lean.Compiler.atMostOnce.Visitor

instance Lean.Compiler.atMostOnce.instAndThenVisitor : AndThen Lean.Compiler.atMostOnce.Visitor

@[inline]

def Lean.Compiler.atMostOnce.skip : Lean.Compiler.atMostOnce.Visitor

@[inline]

def Lean.Compiler.atMostOnce.visitFVar (x : Lean.FVarId) (y : Lean.FVarId) : Lean.Compiler.atMostOnce.Visitor

def Lean.Compiler.atMostOnce.visit (x : Lean.FVarId) : Lean.Expr → Lean.Compiler.atMostOnce.Visitor

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.atMostOnce.visit x (Lean.Expr.fvar y) = Lean.Compiler.atMostOnce.visitFVar y x
• Lean.Compiler.atMostOnce.visit x (Lean.Expr.app f a) = HAndThen.hAndThen (Lean.Compiler.atMostOnce.visit x a) fun x => Lean.Compiler.atMostOnce.visit x f
• Lean.Compiler.atMostOnce.visit x (Lean.Expr.lam binderName d b binderInfo) = HAndThen.hAndThen (Lean.Compiler.atMostOnce.visit x d) fun x => Lean.Compiler.atMostOnce.visit x b
• Lean.Compiler.atMostOnce.visit x (Lean.Expr.forallE binderName d b binderInfo) = HAndThen.hAndThen (Lean.Compiler.atMostOnce.visit x d) fun x => Lean.Compiler.atMostOnce.visit x b
• Lean.Compiler.atMostOnce.visit x (Lean.Expr.mdata data e) = Lean.Compiler.atMostOnce.visit x e
• Lean.Compiler.atMostOnce.visit x (Lean.Expr.proj typeName idx e) = Lean.Compiler.atMostOnce.visit x e
• Lean.Compiler.atMostOnce.visit x x = Lean.Compiler.atMostOnce.skip

@[export lean_at_most_once]

def Lean.Compiler.atMostOnce (e : Lean.Expr) (x : Lean.FVarId) : Bool

Return true iff the free variable with id x occurs at most once in e