Documentation

Lean.Meta.Tactic.Acyclic

source
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.

Instances For
    source
    def Lean.MVarId.acyclic.go (mvarId : Lean.MVarId) (h : Lean.Expr) (lhs : Lean.Expr) (rhs : Lean.Expr) :
    Lean.MetaM Bool
    Instances For