暗黙の引数を無効にして @ をつけたくなるケースとは？

[Seasawher]

いい例があったら紹介したい。

[Seasawher]

これは名前付き引数として与えたくなるケース

abbrev Pos := { n : Nat // n > 0 }

private def Pos.le (x y : Pos) : Prop :=
  x.val ≤ y.val

instance : LE Pos where
  le x y := Pos.le x y

instance : DecidableRel (α := Pos) (· ≤ ·) := by
  dsimp [(· ≤ ·)]
  dsimp [Pos.le]
  infer_instance