Zulip Chat Archive

Stream: general

Topic: rewrite fails


Kevin Buzzard (Mar 14 2019 at 23:17):

import algebra.archimedean
import topology.algebra.ordered

variables {β : Type*} [discrete_linear_ordered_field β] [floor_ring β] [topological_space β]
  [orderable_topology β]

open filter

def digit (b : ) (r : β) (i : ) :  := 37

theorem expansion_tendsto {b : } (hb : 1 < b) (r : β) (N : ) :
  tendsto (λ n : , finset.sum (finset.range n)
    (λ i, (digit b r i : β) * b ^ (n - 1 - i) / b ^ n))
    at_top (nhds (fract r)) :=
begin
  -- rw tendsto_orderable, -- why does this fail?
  /-
  invalid rewrite tactic, failed to synthesize type class instance
  -/
  apply tendsto_orderable.2, -- works fine, now 3 goals
    swap, apply_instance, swap, apply_instance, -- type class inference deals with two
  sorry
end

Why does the rewrite fail?

Kevin Buzzard (Mar 14 2019 at 23:17):

Type class inference can find all the relevant instances.

Chris Hughes (Mar 14 2019 at 23:30):

I don't know why, but sometimes rw @tendsto_orderable \b _ _ _ _ works


Last updated: Dec 20 2023 at 11:08 UTC