Documentation

Lean.Elab.BuiltinDo.Let

source
inductive Lean.Elab.Do.LetOrReassign :
Type
Instances For
    source
    def Lean.Elab.Do.LetOrReassign.getLetMutTk? (letOrReassign : LetOrReassign) :
    Option Syntax
    Instances For
      source
      def Lean.Elab.Do.LetOrReassign.checkMutVars (letOrReassign : LetOrReassign) (vars : Array Ident) :
      DoElabM Unit
      Instances For
        source
        def Lean.Elab.Do.LetOrReassign.registerReassignAliasInfo (letOrReassign : LetOrReassign) (vars : Array Ident) :
        DoElabM Unit
        Instances For
          source
          def Lean.Elab.Do.elabDoLetOrReassignWith (hint : MessageData) (letOrReassign : LetOrReassign) (vars : Array Ident) (k : DoElabM Expr) (elabBody : Term → TermElabM Expr) :
          DoElabM Expr
          Instances For
            source
            def Lean.Elab.Do.elabWithReassignments (letOrReassign : LetOrReassign) (vars : Array Ident) (k : DoElabM Expr) :
            DoElabM Expr
            Instances For
              source
              partial def Lean.Elab.Do.elabDoLetOrReassign (letOrReassign : LetOrReassign) (decl : TSyntax `Lean.Parser.Term.letDecl) (dec : DoElemCont) :
              DoElabM Expr
              source
              def Lean.Elab.Do.elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [`Lean.Parser.Term.doIdDecl, `Lean.Parser.Term.doPatDecl]) (dec : DoElemCont) :
              DoElabM Expr
              Instances For
                source
                def Lean.Elab.Do.elabDoLet :
                DoElab
                Instances For
                  source
                  def Lean.Elab.Do.elabDoHave :
                  DoElab
                  Instances For
                    source
                    def Lean.Elab.Do.elabDoLetRec :
                    DoElab
                    Instances For
                      source
                      def Lean.Elab.Do.elabDoReassign :
                      DoElab
                      Instances For
                        source
                        def Lean.Elab.Do.elabDoLetElse :
                        DoElab
                        Instances For
                          source
                          def Lean.Elab.Do.elabDoLetArrow :
                          DoElab
                          Instances For
                            source
                            def Lean.Elab.Do.elabDoReassignArrow :
                            DoElab
                            Instances For