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