# Documentation

Lean.Meta.Tactic.Acyclic

Close the given goal if h is a proof for an equality such as as = a :: as. Inductive datatypes in Lean are acyclic.

Equations
• One or more equations did not get rendered due to their size.
def Lean.MVarId.acyclic.go (mvarId : Lean.MVarId) (h : Lean.Expr) (lhs : Lean.Expr) (rhs : Lean.Expr) :
Equations
• One or more equations did not get rendered due to their size.