Таким образом, у нас могут быть явные аргументы, обозначаемые ().
Мы также можем иметь неявные аргументы, обозначаемые {}.
Все идет нормально.
Однако зачем нам также нужна [] нотация конкретно для классов типов?
В чем разница между следующими двумя:
theorem foo {x : Type} : ∀s : inhabited x, x := sorry
theorem foo' {x : Type} [s : inhabited x] : x := sorry
Неявные аргументы автоматически вставляются разработчиком Lean. {x : Type}, который появляется в обоих ваших определениях, является одним из примеров неявного аргумента: если у вас есть s : inhabited nat, вы можете написать foo s, что будет уточнено до термина типа nat, потому что аргумент x может быть выведен из s.
Аргументы класса типа - это еще один вид неявных аргументов. Вместо того, чтобы выводиться из более поздних аргументов, разработчик запускает процедуру, называемую разрешением класса типа, которая пытается сгенерировать термин указанного типа. (См. Главу 10 https://leanprover.github.io/theorem_proving_in_lean_theorem_proving. a>.) Итак, ваш foo' вообще не принимает аргументов. Если ожидаемый тип x может быть выведен из контекста, Lean будет искать экземпляр inhabited x и вставлять его:
def foo' {x : Type} [s : inhabited x] : x := default x
instance inh_nat : inhabited nat := ⟨3⟩
#eval (2 : ℕ) + foo' -- 5
Здесь Lean делает вывод, что x должно быть nat, и находит и вставляет экземпляр inhabited nat, так что foo' сам по себе уточняется до термина типа nat.
