PG
если прочитаю пейперы по теме в ближайший год тегну тебя
Size: a a a
2020 August 26
χλ
если прочитаю пейперы по теме в ближайший год тегну тебя
2020?
Окей
Окей
χλ
А я набросать чуток позже попробую чего-нибудь
SA
with all due respect
SA
вот теперь они будут изобретать свой коалтон на схемах
SA
вот атк вот оно все у нас
SA
χλ
V(
но они конечно же называют его "си-оу-си"
PG
CiC
PG
PG
синктаксически похоже на Lean
SA
ну оно лиспоподобное
SA
но я честно говоря не разбирался
SA
я в какой то момент очень был в теме хайпа про всякие там системы типов продвинутые ноо
SA
уже нет
SA
мне впрочем вполне интересно че у них выйдет но писать на этом я не факт что хочу)
PG
а вот этом что-то есть
PG
ну то есть понятно что в Coq/Lean/Agda можно менять парсер на ходу
PG
и тут тоже