Documentation

Lean.Elab.BindersUtil

source
def Lean.Elab.Term.expandOptType (ref optType : Lean.Syntax) :
Lean.Syntax

Recall that

def typeSpec := leading_parser " : " >> termParser
def optType : Parser := optional typeSpec
Instances For
    source
    def Lean.Elab.Term.getMatchAltsNumPatterns (matchAlts : Lean.Syntax) :
    Nat

    Helper function for expandEqnsIntoMatch

    Instances For
      source
      def Lean.Elab.Term.expandMatchAlt (stx : Lean.TSyntax `Lean.Parser.Term.matchAlt) :
      Lean.MacroM (Array (Lean.TSyntax `Lean.Parser.Term.matchAlt))

      Expand a match alternative such as | 0 | 1 => rhs to an array containing | 0 => rhs and | 1 => rhs.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Elab.Term.shouldExpandMatchAlt :
        Lean.TSyntax `Lean.Parser.Term.matchAlt → Bool
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Elab.Term.expandMatchAlts? (stx : Lean.Syntax) :
          Lean.MacroM (Option Lean.Syntax)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean.Elab.Term.clearInMatchAlt (stx : Lean.TSyntax `Lean.Parser.Term.matchAlt) (vars : Array Lean.Ident) :
            Lean.TSyntax `Lean.Parser.Term.matchAlt
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Lean.Elab.Term.clearInMatch (stx : Lean.Syntax) (vars : Array Lean.Ident) :
              Lean.MacroM Lean.Syntax
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For