ID
То бишь мы задаем n = 5 как параметр, и оно уходит в бесконечную рекурсию?
Size: a a a
2021 May 27
ID
Стоп
ID
Увидел
ID
n : nat это типа n -- натуральное?а
да
а
Переслано от а это кто
уточню что в Coq натуральные числа определены как рекурсивный тип (раст синтаксис)
enum nat {
O,
S(nat),
}
первый вариант означает что число равно нулю, вторая означает что число равно 1 + число внутриа
Не, n будет уменьшатся и в конечном итоге станет 0, рекурсия закончится
ID
Я про bad_factotial
ID
Там где -10
ID
А какой движок отвечает за вывод этого всего?
а
Если n = 5, то n - 10 будет меньше 5, а точнее будет равно нулю, произойдёт один рекурсивный вызов в котором
match n withВыберет первую ветку и рекурсия закончится вернув 0
| O => O
| ....
end
ID
Ок, спасибо
а
Ядро Coq написано на OCaml. Движок по сути является интерпретатором типизированного лямбда-исчисления
а
только там не лямбда-исчисление, а исчисление индуктивных конструкций
https://en.wikipedia.org/wiki/Calculus_of_constructions
https://en.wikipedia.org/wiki/Calculus_of_constructions
ID
Все, сильно заумное что-то пошло... 😅
а
xd
KR
Просто делай тогда на OctoberCMS
ID
Не понял. Я шо, пхпшник по твоему, или шо
C
лох не мамонт