Documentation

Lean.Meta.Tactic.Acyclic

source
def Lean.Meta.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.
source
def Lean.Meta.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.