def Lean.MVarId.acyclic (mvarId : MVarId) (h : Expr) : 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 : MVarId) (h lhs rhs : Expr) : MetaM Bool

Equations

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