Documentation

Lean.Elab.BuiltinDo.Match

source
def Lean.Elab.Do.withElaboratedLHS {α : Type} (patternVarDecls : Array Term.PatternVarDecl) (patternStxs : Array Syntax) (lhsStx : Syntax) (discrTypes : Array Expr) (k : Meta.Match.AltLHS → TermElabM α) :
TermElabM α
Instances For
    source
    def Lean.Elab.Do.isSyntaxMatch (alts : Array (TSyntax `Lean.Parser.Term.matchAlt)) :
    Bool
    Instances For
      source
      def Lean.Elab.Do.getAltsPatternVars (alts : TSyntaxArray `Lean.Parser.Term.matchAlt) :
      TermElabM (Array Ident)
      Instances For
        source
        def Lean.Elab.Do.elabDoMatch :
        DoElab
        Instances For