ЗП
вчера я конечно сделал Hello World
Size: a a a
2018 January 12
🦉
вы с какой, блядь, планеты?!
PG
Здесь легитимно
PG
Я с этой, а очки для сварки на стройке нашел
ЗП
кстати как с леан проще?) а то я вчера все проклял пока агду поставил и еще ничего кроме подсветки в vscode нет
PG
У меня такой сетоид получается:
RelOn : Type -> Type
interface (Reflexive R, Symmetric R, Transitive R) =>
Equivalence (R : RelOn a) where
record Setoid where
constructor MkSetoid
carrier : Type
equality : RelOn carrier
equalityIsEquivalence : Equivalence equality
к
кстати как с леан проще?) а то я вчера все проклял пока агду поставил и еще ничего кроме подсветки в vscode нет
lean очень легко ставиться и для vscode офигенный плагин
к
ну и сам по себе мне lean показался очень простым в плане синтаксиса и скорости вхождения, некоторые конструкции пишешь чисто "а вдруг" и они работают как ожидается
к
но говорят, что падает с сегфолтами
A
кстати как с леан проще?) а то я вчера все проклял пока агду поставил и еще ничего кроме подсветки в vscode нет
Насчёт агды: у меня всё очень просто встало. В емаксе всё работает, ну это как всегда.
ЗП
AT
но говорят, что падает с сегфолтами
причем регулярно
AT
недавно Лео написал ЧаВо, где посылает лесом всех желающих контрибутить в lean
ЕО
А что у лина с доказательной силой? Агда идакшн-рекаршн умеет, иерархию универсумов и х-м по их уровням
AT
лин же во многом содран с кока, многое есть, но induction-recirsion раньше не было (в коке тоже пока нет, но работы идут)
AT
или лучше сказать, что они реализуют систему, основанную на CIC
ЗП
вроде к лин кубическая тт появилась?
AT
не слышал, они HoTT дропнули пару лет назад