hints needed

[holtzermann17]

Without hints I get errors like:

---

ambiguous overload, possible interpretations 2 + 2 2 + 2 Additional information: /home/joe/theorem_proving_in_lean_examples/10_3.lean:17:9: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available

[avigad]

@holtzermann17 These work in the online version and in my own version of Lean. My guess is that again you had some other things in the file that led to the ambiguity. Can you reproduce the problem?

[holtzermann17]

Yes, I did indeed have the previous block in, including a namespace hidden that wasn't in the -- BEGIN/-- END scope. So, a similar situation to #77. So there are two versions of add floating around. #check hidden.add 2 2 is not ambiguous. So, new thought -- rather than changing the code maybe the surrounding text could change slightly. At the moment, when it says

We can then declare instances for nat, and bool

it sounds like that's something that can be added cleanly to the previous block. And, indeed, it can, in the standard library, but not here b/c the standard library is visible. I'm not quite sure what it should say.

universes u

namespace hidden

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 2 + 2    -- nat
#check tt + ff  -- bool
end hidden