Documentation

Lean.Util.ReplaceExpr

Instances For
    Equations
    Instances For
      @[inline]
      Equations
      Instances For
        @[inline]
        Equations
        • c.resultIdx key = c.keyIdx key + c.size
        Instances For
          @[inline]
          Equations
          • c.hasResultFor key = let_fun this := ; ptrEq (unsafeCast key) c.keysResults[c.keyIdx key]
          Instances For
            @[inline]
            Equations
            • c.getResultFor key = let_fun this := ; unsafeCast c.keysResults[c.resultIdx key]
            Instances For
              Equations
              • c.store key result = { size := c.size, keysResults := (c.keysResults.uset (c.keyIdx key) (unsafeCast key) ).uset (c.resultIdx key) (unsafeCast result) }
              Instances For
                @[inline]
                Equations
                Instances For
                  @[specialize #[]]
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[specialize #[]]
                    Instances For
                      @[implemented_by Lean.Expr.ReplaceImpl.replaceUnsafe]
                      Equations
                      Instances For