Equations
- One or more equations did not get rendered due to their size.
Instances For
Implementation of arg 0
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Elab.Tactic.Conv.congrArgForall
(tacticName : String)
(domain : Bool)
(mvarId : MVarId)
(lhs rhs : Expr)
:
Implements arg
for foralls. If domain
is true, accesses the domain, otherwise accesses the codomain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Lean.Elab.Tactic.Conv.extLetBodyCongr? mvarId lhs rhs = pure none
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.