Documentation

Lean.Meta.Match.MVarRenaming

source
structure Lean.Meta.MVarRenaming :
Type

A mapping from MVarId to MVarId

Instances For
    source
    def Lean.Meta.MVarRenaming.isEmpty (s : MVarRenaming) :
    Bool
    Equations
      Instances For
        source
        def Lean.Meta.MVarRenaming.find? (s : MVarRenaming) (mvarId : MVarId) :
        Option MVarId
        Equations
          Instances For
            source
            def Lean.Meta.MVarRenaming.find! (s : MVarRenaming) (mvarId : MVarId) :
            MVarId
            Equations
              Instances For
                source
                def Lean.Meta.MVarRenaming.insert (s : MVarRenaming) (mvarId mvarId' : MVarId) :
                MVarRenaming
                Equations
                  Instances For
                    source
                    def Lean.Meta.MVarRenaming.apply (s : MVarRenaming) (e : Expr) :
                    Expr
                    Equations
                      Instances For