structure Lean.Compiler.atMostOnce.AtMostOnceData : Type

• found : Bool
• result : Bool

def Lean.Compiler.atMostOnce.Visitor : Type

Equations

• Lean.Compiler.atMostOnce.Visitor = (Lean.Compiler.atMostOnce.AtMostOnceData → Lean.Compiler.atMostOnce.AtMostOnceData)

Instances For

• Lean.Compiler.atMostOnce.instAndThenVisitor

@[inline]

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

Equations

• Lean.Compiler.atMostOnce.seq f g d = match f d with | { found := found, result := false } => { found := found, result := false } | other => g other

instance Lean.Compiler.atMostOnce.instAndThenVisitor : AndThen Visitor

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lean.Compiler.atMostOnce.skip : Visitor

Equations

• Lean.Compiler.atMostOnce.skip = id

@[inline]

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

Equations

• Lean.Compiler.atMostOnce.visitFVar x y { found := found, result := false } = { found := found, result := false }
• Lean.Compiler.atMostOnce.visitFVar x y { found := false, result := true } = { found := x == y, result := true }
• Lean.Compiler.atMostOnce.visitFVar x y { found := true, result := true } = { found := true, result := x != y }

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

Equations

• Lean.Compiler.atMostOnce.visit x (Lean.Expr.fvar y) = Lean.Compiler.atMostOnce.visitFVar y x
• Lean.Compiler.atMostOnce.visit x (f.app a) = Lean.Compiler.atMostOnce.visit x a >> Lean.Compiler.atMostOnce.visit x f
• Lean.Compiler.atMostOnce.visit x (Lean.Expr.lam binderName d b binderInfo) = Lean.Compiler.atMostOnce.visit x d >> Lean.Compiler.atMostOnce.visit x b
• Lean.Compiler.atMostOnce.visit x (Lean.Expr.forallE binderName d b binderInfo) = Lean.Compiler.atMostOnce.visit x d >> Lean.Compiler.atMostOnce.visit x b
• Lean.Compiler.atMostOnce.visit x (Lean.Expr.letE declName t v b nonDep) = Lean.Compiler.atMostOnce.visit x t >> Lean.Compiler.atMostOnce.visit x v >> 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 : Expr) (x : FVarId) : Bool

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

Equations

• Lean.Compiler.atMostOnce e x = match Lean.Compiler.atMostOnce.visit x e { found := false, result := true } with | { found := found, result := result } => result