TorchLean API

Docs HomeGuideExamplesGraphs

Aesop.RuleTac.FVarIdSubst

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