Пропозиции вместо булевых значений

В TypeScript логические выражения имеют единый тип boolean с двумя значениями (true/false) и сразу сворачиваются в значение.

В Lean логические выражения имеют тип Prop и не вычисляются автоматически в true/false.

Пропозиция в Lean является одновременно значением и типом, и её доказательство — это значение этого типа.

Чтобы доказать пропозицию в Lean, необходимо предоставить доказательство (value of type Prop), например, с помощью by rfl или by decide.

Невозможность получить доказательство пропозиции означает её ложность (или недоказуемость), а её отрицание можно доказать как отдельную пропозицию.

Все доказательства одной пропозиции считаются эквивалентными (proof irrelevance) независимо от метода их получения.