VL
nice coq awesome users
Size: a a a
2020 May 15
A
как по мне это аксиома)
Ну мы тут уже подходим к Спинозе
A
Кто-нибудь Этику Спинозы переводил в Coq?
AP
Artem
Ну мы тут уже подходим к Спинозе
А спиноза что толковал на этот счет? )
VL
я бы юзерам вообще не разрешал за комп садиться
VL
это слишком сложно для них
A
А спиноза что толковал на этот счет? )
Насчёт call/cc?
AP
Artem
Насчёт call/cc?
Насчет Coq. что касается call/cc там все прозрачно и элементарно, че там толковать-то можно )
AP
Artem
Вот Coq заебись тема.
Написана на OCaml; C
AP
А что не на лиспах?
VL
Artem
Кто-нибудь Этику Спинозы переводил в Coq?
а этику аристотеля?
VL
или канта?
AP
Теоретической базой Coq считается исчисление конструкций; в названии скрыта его аббревиатура (CoC, англ. calculus of constructions) и сокращение от фамилии создателя исчисления — Тьерри Кокана.
AP
Че оно, теорему Ферма докажет? )
A
а этику аристотеля?
Спинозы легче перевести, она написана же как постулаты + доказательства теорем
A
Че оно, теорему Ферма докажет? )
Поможет
AP
DL
Зачетный фильм, надо пересмотреть )
лол, только что это обсуждали, я решил, что наверное не стоит, бо гарантированы фейспалмы