not eager placeholder in implicit argument

Stream: new members

[Shanghe Chen]

Hi in TPIL More on Implicit Arguments how the weaker notation solves the placeholder in the following example?

def reflexive {α : Type u} (r : α → α → Prop) : Prop :=
  ∀ (a : α), r a a

def symmetric {α : Type u} (r : α → α → Prop) : Prop :=
-- why makeing this not eagerly solving the problem in thm3?
∀ {{a b : α}}, r a b → r b a

def transitive {α : Type u} (r : α → α → Prop) : Prop :=
-- why makeing this not eagerly solving the problem in thm3?
∀ {{a b c : α}}, r a b → r b c → r a c

def euclidean {α : Type u} (r : α → α → Prop) : Prop :=
-- why makeing this not eagerly solving the problem in thm3?
∀ {{a b c : α}}, r a b → r a c → r b c

theorem th1 {α : Type u} {r : α → α → Prop}
(reflr : reflexive r) (euclr : euclidean r)
: symmetric r :=
fun {a b : α} =>
fun (h : r a b) =>
show r b a from euclr h (reflr _)

theorem th2 {α : Type u} {r : α → α → Prop}
(symmr : symmetric r) (euclr : euclidean r)
: transitive r :=
fun {a b c : α} =>
fun (rab : r a b) (rbc : r b c) =>
euclr (symmr rab) rbc

theorem th3 {α : Type u} {r : α → α → Prop}
(reflr : reflexive r) (euclr : euclidean r)
            : transitive r :=
  th2 (th1 reflr euclr) euclr

[Shanghe Chen]

Originally it has to be @th2 _ _ (@th1 _ _ reflr @euclr) @euclr in th3

[Timo Carlin-Burns]

That example is a bit confusing and I have a pull request open to fix it. In fact, even before changing the brackets to {{}}, th3 can be th2 (th1 reflr @euclr) @euclr. The weaker implicit arguments only remove the need for @ before euclr.