@[inline]
def
Lean.Compiler.atMostOnce.seq
(f : Lean.Compiler.atMostOnce.Visitor)
(g : Lean.Compiler.atMostOnce.Visitor)
:
Instances For
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
Instances For
@[export lean_at_most_once]
Return true iff the free variable with id x
occurs at most once in e