def Lean.Elab.Do.elabDoIdDecl (x : Ident) (xType? : Option Term) (rhs : TSyntax `doElem) (k : DoElabM Expr) (kind : DoElemContKind := DoElemContKind.nonDuplicable) : DoElabM Expr

Equations

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