ΛВ
ну норм
а в дотте арифметика на тайплевеле как сделана?
Size: a a a
2021 March 14
ΛВ
видел там какой-то типа черчевый ноль
Oℕ
думаешь ошибка в ожидаемом результате?
надо анфолдить
ΛВ
и на матч типах сложение вычитание
ΛВ
но не напрямую черч намберс же
Oℕ
это тебе не идрис аренд
R
а как ето сделать в вскоке
Oℕ
я не пойму чо ты делаешь
R
я проверяю умножение
V
The term "eq_refl" has type
"muln (S (S O)) (S (S O)) = muln (S (S O)) (S (S O))"
while it is expected to have type
"muln (S (S O)) (S (S O)) = S (S (S (S O)))"
(cannot unify "muln (S (S O)) (S (S O))" and "S (S (S (S O)))”).
SSOSATb
R
написал я ево криво
R
как
беру операции и сравниваю с ожидаемым значением
λ
если бы кот всегда был рядом....
Естли бы ты не предавал...
Oℕ
напиши
Lemma ratten: 2 * 2 = 4.
Proof. done.Qed.
Lemma ratten: 2 * 2 = 4.
Proof. done.Qed.
R
Естли бы ты не предавал...
сегодня были дела
R
в 9 уже в метро был
R
милостыню просил