structure Lean.Compiler.atMostOnce.AtMostOnceData : Type

• found : Bool
• result : Bool

def Lean.Compiler.atMostOnce.Visitor : Type

@[inline]

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

instance Lean.Compiler.atMostOnce.instAndThenVisitor : AndThen Visitor

@[inline]

def Lean.Compiler.atMostOnce.skip : Visitor

@[inline]

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

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

@[export lean_at_most_once]

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

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