K
Он его не забыл, он его удолил
N = a -> (a -> a) -> a
zero z s = z
succ t z s = s t
Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
505 membersпожаловаться на группу
2021 November 13
K
[
Можно типы zero и succ?
ПС
А вообще, конечно, это рекурсор, а не элиминатор
Элиминатор вот
natElim : (T : Nat -> Type) -> (z : T zero) -> (s : (n : Nat) -> T n -> T (suc n)) -> (n : Nat) -> T n
natElim _ z _ zero = z
natElim T z s (suc n) = s n (natElim T z s n)
Элиминатор вот
natElim : (T : Nat -> Type) -> (z : T zero) -> (s : (n : Nat) -> T n -> T (suc n)) -> (n : Nat) -> T n
natElim _ z _ zero = z
natElim T z s (suc n) = s n (natElim T z s n)
K
zero :: N
succ :: N -> N
K
Это конструкторы
O и SЗП
Зигохистоморфный Пре... in Типы в языках программирования, моделирования, представления знаний и жизни
еще можно судить это с точки зрения двойного отрицания, что есть мост для перехода от классической логики к интуиционистской
ПС
В каком месте это
((a -> _|_) -> _|_) -> a?АП
читаю, в электронном виде
[
А у него - в бумажном! Вот он и хвастается
ЗП
Зигохистоморфный Пре... in Типы в языках программирования, моделирования, представления знаний и жизни
у меня тоже в бумажном, но я сам печатал
KR
@GabrielFallen очередной бот ^^^^