dec_trivial is ambiguous in example for Chapter 10, Type Classes

[holtzermann17]

example : 1 ≠ 0 ∧ (5 < 2 ∨ 3 < 7) := dec_trivial

gives me this:

---

ambiguous overload, possible interpretations of_as_true ?m_3 of_as_true ?m_6 Additional information: /home/joe/theorem_proving_in_lean_examples/10_7.lean:20:37: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because it failed to disambiguate overload using the expected type 1 ≠ 0 ∧ (5 < 2 ∨ 3 < 7) the following overloaded terms were applicable of_as_true ?m_18 of_as_true ?m_21

[avigad]

This works for me in my browser version, as well as in my native 3.4.1 version of Lean. Perhaps there were other things in your file that led to the ambiguity? If you copied the snippet above it, that would explain the ambiguity.

[holtzermann17]

Right, that's what I did. I hadn't paid attention to "The standard library introduces the following definitions and notation" (emphasis added), above that previous snippet. I've been in the habit of redefining standard functions when I examine the snippets in the book, e.g., my_as_true, my_of_as_true, but did not think to try

notation `my_dec_trivial` := my_of_as_true (by tactic.triv)
example : 1 ≠ 0 ∧ (5 < 2 ∨ 3 < 7) := my_dec_trivial

Hence the error (but fixed with that!)