Documentation

Lean.Elab.Do.PatternVar

source
def Lean.Elab.Do.getPatternVarsEx (pattern : Term) :
TermElabM (Array Ident)
Instances For
    source
    def Lean.Elab.Do.getPatternsVarsEx (patterns : Array Term) :
    TermElabM (Array Ident)
    Instances For
      source
      def Lean.Elab.Do.getLetIdDeclVars (letIdDecl : TSyntax `Lean.Parser.Term.letIdDecl) :
      TermElabM (Array Ident)
      Instances For
        source
        def Lean.Elab.Do.getLetPatDeclVars (letPatDecl : TSyntax `Lean.Parser.Term.letPatDecl) :
        TermElabM (Array Ident)
        Instances For
          source
          def Lean.Elab.Do.getLetDeclVars (letDecl : TSyntax `Lean.Parser.Term.letDecl) :
          TermElabM (Array Ident)
          Instances For
            source
            def Lean.Elab.Do.getLetRecDeclsVars (letRecDecls : TSyntax `Lean.Parser.Term.letRecDecls) :
            TermElabM (Array Ident)
            Instances For
              source
              def Lean.Elab.Do.getExprPatternVarsEx (exprPattern : TSyntax `Lean.Parser.Term.matchExprPat) :
              TermElabM (Array Ident)
              Instances For