revise instructions where sample code repeats standard library defs to avoid ambiguity

I ran into trouble in similar ways in #76 and #77 with two bits of sample code that redefine standard library components. Is there a way to adjust the way these examples are treated, to help the reader avoid ambiguity? E.g., in #77, if the duplicate add is defined in the hidden namespace, #check hidden.add 2 2 is not ambiguous. One possibility would be to incorporate the error into the sample code with a comment.

universes u

namespace hidden
-- just a binary function from the type to itself?  Wow
class has_add (α : Type u) :=
(add : α → α → α)

def add {α : Type u} [has_add α] : α → α → α := has_add.add

notation a ` + ` b := add a b

instance nat_has_add : has_add nat :=
⟨nat.add⟩

instance bool_has_add : has_add bool :=
⟨bor⟩

#check hidden.add 2  2    -- nat

-- This will fail because the code duplicates the standard library and
-- there are two applicable versions of + that are visible here.
#check 2 + 2 

-- There is only one visible version of + applicable in this case.
#check tt + ff  -- bool
end hidden

leanprover / theorem_proving_in_lean

revise instructions where sample code repeats standard library defs to avoid ambiguity #78