def Lean.MVarId.acyclic (mvarId : Lean.MVarId) (h : Lean.Expr) : Lean.MetaM Bool

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) : Lean.MetaM Bool

Equations

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