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
    Instances For
      source
      def Lean.Meta.MVarRenaming.find? (s : MVarRenaming) (mvarId : MVarId) :
      Option MVarId
      Instances For
        source
        def Lean.Meta.MVarRenaming.find! (s : MVarRenaming) (mvarId : MVarId) :
        MVarId
        Instances For
          source
          def Lean.Meta.MVarRenaming.insert (s : MVarRenaming) (mvarId mvarId' : MVarId) :
          MVarRenaming
          Instances For
            source
            def Lean.Meta.MVarRenaming.apply (s : MVarRenaming) (e : Expr) :
            Expr
            Instances For