кортеж это И

то есть первая задача формулируется как

(t -> t -> u) && ((t -> u) -> t) -> u

мда я примерно понимаю как за это цепляться но сложно

Ммм, лосятина тушеная с зеленым перцем это вкусняшка. Рекомендую 😁

а как третье решается? там же ничего не подставишь вообще

ээм это должно работать?

ну ты обработал все кейсы энума - почему не должно?

"из лжи следует что угодно" (с)

потому что нужно вернуть T

все 0 веток возвращают T

но Т это конкретный тип не?

не веришь мне спрсои тайпчекера

или эти законы тут не работают

всё работает, можно вернуть любой T

Ну например у тебя есть выражение в программе:
(x | true) | y
И ты хочешь доказать что это утверждение всегда будет выдавать true. Для этого тебе необходимо утверждение для доказательства, например
f x y = (x | true) | y // функция

forall x, y then f x y == true

То есть для любых x y результат выражения будет true

Потом ты собственно доказываешь это. Например:
start
ir1 = x | true.
forall x then ir1 = true.
ir2 = ir1 | y
forall y then ir2 = true.
end

Могут быть неточности в моем объяснении, но в целом этот процесс так происходит

Маленькая заблудившаяся пельмешка 😁

бля что за бред лол, как инстанцировать пустой энам, как это вообще предполагается будет работать

Добро пожаловать в раст

и что возвращает  match a {}