def Lean.Elab.Do.withElaboratedLHS {α : Type} (patternVarDecls : Array Term.PatternVarDecl) (patternStxs : Array Syntax) (lhsStx : Syntax) (numDiscrs : Nat) (matchType : Expr) (k : Meta.Match.AltLHS → TermElabM α) : TermElabM α

Equations

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

def Lean.Elab.Do.isSyntaxMatch (alts : Array (TSyntax `Lean.Parser.Term.matchAlt)) : Bool

Equations

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

def Lean.Elab.Do.getAltsPatternVars (alts : TSyntaxArray `Lean.Parser.Term.matchAlt) : TermElabM (Array Ident)

Equations

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

def Lean.Elab.Do.elabDoMatch : DoElab

Equations

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