Documentation

Lean.Elab.Do.Switch

source
opaque Lean.Elab.Term.backward.do.legacy :
Lean.Option Bool
source
def Lean.Elab.Term.expandTermFor :
Macro
Equations
Instances For
    source
    def Lean.Elab.Term.expandTermTry :
    Macro
    Equations
    Instances For
      source
      def Lean.Elab.Term.expandTermUnless :
      Macro
      Equations
      Instances For
        source
        def Lean.Elab.Term.expandTermReturn :
        Macro
        Equations
        Instances For
          source
          def Lean.Elab.Term.elabDo :
          TermElab
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean.Elab.Term.elabTermLiftMethod :
            TermElab
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For