def Lean.Elab.Do.getPatternVarsEx (pattern : Term) : TermElabM (Array Ident)

Equations

• Lean.Elab.Do.getPatternVarsEx pattern = do let a ← Lean.Elab.Term.getPatternVars pattern.raw <|> Lean.Elab.Term.Quotation.getPatternVars pattern.raw pure (Lean.TSyntaxArray.mk a)

def Lean.Elab.Do.getPatternsVarsEx (patterns : Array Term) : TermElabM (Array Ident)

Equations

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

def Lean.Elab.Do.getLetIdDeclVars (letIdDecl : TSyntax `Lean.Parser.Term.letIdDecl) : TermElabM (Array Ident)

Equations

• Lean.Elab.Do.getLetIdDeclVars letIdDecl = Lean.Elab.Do.getLetIdVars✝ { raw := letIdDecl.raw[0] }

def Lean.Elab.Do.getLetPatDeclVars (letPatDecl : TSyntax `Lean.Parser.Term.letPatDecl) : TermElabM (Array Ident)

Equations

• Lean.Elab.Do.getLetPatDeclVars letPatDecl = Lean.Elab.Do.getPatternVarsEx { raw := letPatDecl.raw[0] }

def Lean.Elab.Do.getLetDeclVars (letDecl : TSyntax `Lean.Parser.Term.letDecl) : TermElabM (Array Ident)

Equations

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

def Lean.Elab.Do.getLetRecDeclsVars (letRecDecls : TSyntax `Lean.Parser.Term.letRecDecls) : TermElabM (Array Ident)

Equations

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

def Lean.Elab.Do.getExprPatternVarsEx (exprPattern : TSyntax `Lean.Parser.Term.matchExprPat) : TermElabM (Array Ident)

Equations

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