Documentation

Aesop.RuleTac.FVarIdSubst

source
structure Aesop.FVarIdSubst :
Type
Instances For
    source
    instance Aesop.instInhabitedFVarIdSubst :
    Inhabited FVarIdSubst
    Equations
      source
      def Aesop.FVarIdSubst.isEmpty (s : FVarIdSubst) :
      Bool
      Equations
        Instances For
          source
          def Aesop.FVarIdSubst.contains (s : FVarIdSubst) (fvarId : Lean.FVarId) :
          Bool
          Equations
            Instances For
              source
              def Aesop.FVarIdSubst.find? (s : FVarIdSubst) (fvarId : Lean.FVarId) :
              Option Lean.FVarId
              Equations
                Instances For
                  source
                  def Aesop.FVarIdSubst.get (s : FVarIdSubst) (fvarId : Lean.FVarId) :
                  Lean.FVarId
                  Equations
                    Instances For
                      source
                      def Aesop.FVarIdSubst.apply (s : FVarIdSubst) (e : Lean.Expr) :
                      Lean.Expr
                      Equations
                        Instances For
                          source
                          def Aesop.FVarIdSubst.applyToLocalDecl (s : FVarIdSubst) :
                          Lean.LocalDecl → Lean.LocalDecl
                          Equations
                            Instances For
                              source
                              def Aesop.FVarIdSubst.domain (s : FVarIdSubst) :
                              Std.HashSet Lean.FVarId
                              Equations
                                Instances For
                                  source
                                  def Aesop.FVarIdSubst.codomain (s : FVarIdSubst) :
                                  Std.HashSet Lean.FVarId
                                  Equations
                                    Instances For
                                      source
                                      def Aesop.FVarIdSubst.empty :
                                      FVarIdSubst
                                      Equations
                                        Instances For
                                          source
                                          instance Aesop.FVarIdSubst.instEmptyCollection :
                                          EmptyCollection FVarIdSubst
                                          Equations
                                            source
                                            def Aesop.FVarIdSubst.insert (s : FVarIdSubst) (old new : Lean.FVarId) :
                                            FVarIdSubst
                                            Equations
                                              Instances For
                                                source
                                                def Aesop.FVarIdSubst.erase (s : FVarIdSubst) (fvarId : Lean.FVarId) :
                                                FVarIdSubst
                                                Equations
                                                  Instances For
                                                    source
                                                    def Aesop.FVarIdSubst.append (s t : FVarIdSubst) :
                                                    FVarIdSubst
                                                    Equations
                                                      Instances For
                                                        source
                                                        def Aesop.FVarIdSubst.ofFVarSubstIgnoringNonFVarIds (s : Lean.Meta.FVarSubst) :
                                                        FVarIdSubst
                                                        Equations
                                                          Instances For
                                                            source
                                                            def Aesop.FVarIdSubst.ofFVarSubst? (s : Lean.Meta.FVarSubst) :
                                                            Option FVarIdSubst
                                                            Equations
                                                              Instances For