Documentation

Lean.Meta.Tactic.Replace

source
def Lean.MVarId.replaceTargetEq (mvarId : Lean.MVarId) (targetNew : Lean.Expr) (eqProof : Lean.Expr) :
Lean.MetaM Lean.MVarId

Convert the given goal Ctx |- target into Ctx |- targetNew using an equality proof eqProof : target = targetNew. It assumes eqProof has type target = targetNew

Instances For
    source
    @[deprecated Lean.MVarId.replaceTargetEq]
    def Lean.Meta.replaceTargetEq (mvarId : Lean.MVarId) (targetNew : Lean.Expr) (eqProof : Lean.Expr) :
    Lean.MetaM Lean.MVarId
    Instances For
      source
      def Lean.MVarId.replaceTargetDefEq (mvarId : Lean.MVarId) (targetNew : Lean.Expr) :
      Lean.MetaM Lean.MVarId

      Convert the given goal Ctx |- target into Ctx |- targetNew. It assumes the goals are definitionally equal. We use the proof term

      @id target mvarNew

      to create a checkpoint.

      Instances For
        source
        @[deprecated Lean.MVarId.replaceTargetDefEq]
        def Lean.Meta.replaceTargetDefEq (mvarId : Lean.MVarId) (targetNew : Lean.Expr) :
        Lean.MetaM Lean.MVarId
        Instances For
          source
          @[inline, reducible]
          abbrev Lean.MVarId.replaceLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) (eqProof : Lean.Expr) :
          Lean.MetaM Lean.Meta.AssertAfterResult

          Replace type of the local declaration with id fvarId with one with the same user-facing name, but with type typeNew. This method assumes eqProof is a proof that type of fvarId is equal to typeNew. This tactic actually adds a new declaration and (try to) clear the old one. If the old one cannot be cleared, then at least its user-facing name becomes inaccessible. Remark: the new declaration is added immediately after fvarId. typeNew must be well-formed at fvarId, but eqProof may contain variables declared after fvarId.

          Instances For
            source
            @[inline, reducible, deprecated Lean.MVarId.replaceLocalDecl]
            abbrev Lean.Meta.replaceLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) (eqProof : Lean.Expr) :
            Lean.MetaM Lean.Meta.AssertAfterResult
            Instances For
              source
              def Lean.MVarId.replaceLocalDeclDefEq (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) :
              Lean.MetaM Lean.MVarId

              Replace the type of fvarId at mvarId with typeNew. Remark: this method assumes that typeNew is definitionally equal to the current type of fvarId.

              Instances For
                source
                @[deprecated Lean.MVarId.replaceLocalDeclDefEq]
                def Lean.Meta.replaceLocalDeclDefEq (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) :
                Lean.MetaM Lean.MVarId
                Instances For
                  source
                  def Lean.MVarId.change (mvarId : Lean.MVarId) (targetNew : Lean.Expr) (checkDefEq : optParam Bool true) :
                  Lean.MetaM Lean.MVarId

                  Replace the target type of mvarId with typeNew. If checkDefEq = false, this method assumes that typeNew is definitionally equal to the current target type. If checkDefEq = true, throw an error if typeNew is not definitionally equal to the current target type.

                  Instances For
                    source
                    @[deprecated Lean.MVarId.change]
                    def Lean.Meta.change (mvarId : Lean.MVarId) (targetNew : Lean.Expr) (checkDefEq : optParam Bool true) :
                    Lean.MetaM Lean.MVarId
                    Instances For
                      source
                      def Lean.MVarId.changeLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) (checkDefEq : optParam Bool true) :
                      Lean.MetaM Lean.MVarId

                      Replace the type of the free variable fvarId with typeNew. If checkDefEq = false, this method assumes that typeNew is definitionally equal to fvarId type. If checkDefEq = true, throw an error if typeNew is not definitionally equal to fvarId type.

                      Instances For
                        source
                        @[deprecated Lean.MVarId.changeLocalDecl]
                        def Lean.Meta.changeLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) (checkDefEq : optParam Bool true) :
                        Lean.MetaM Lean.MVarId
                        Instances For
                          source
                          def Lean.MVarId.modifyTarget (mvarId : Lean.MVarId) (f : Lean.Expr → Lean.MetaM Lean.Expr) :
                          Lean.MetaM Lean.MVarId

                          Modify mvarId target type using f.

                          Instances For
                            source
                            @[deprecated Lean.Meta.modifyTarget]
                            def Lean.Meta.modifyTarget (mvarId : Lean.MVarId) (f : Lean.Expr → Lean.MetaM Lean.Expr) :
                            Lean.MetaM Lean.MVarId
                            Instances For
                              source
                              def Lean.MVarId.modifyTargetEqLHS (mvarId : Lean.MVarId) (f : Lean.Expr → Lean.MetaM Lean.Expr) :
                              Lean.MetaM Lean.MVarId

                              Modify mvarId target type left-hand-side using f. Throw an error if target type is not an equality.

                              Instances For
                                source
                                @[deprecated Lean.MVarId.modifyTargetEqLHS]
                                def Lean.Meta.modifyTargetEqLHS (mvarId : Lean.MVarId) (f : Lean.Expr → Lean.MetaM Lean.Expr) :
                                Lean.MetaM Lean.MVarId
                                Instances For