X
Мне он привлекательный как учебный язык. Потом переползу на что-нибудь более взрослое
Size: a a a
2021 November 24
X
конкретно устройство типов в lean мне уже нравится гораздо больше, чем в ф*
X
мне интересно, там допускается reasoning about types?
X
мож ты поведаешь?
s
Смотри, я не верю в то, что учиться надо на чём-то ущербном.
X
там есть смысл у фразы "доказать равенство типов"?
X
ну, можно доказать, что
type x = (t:int{ my_predicate t })
это то же самое, что
type y = (t:int{ my_predicate2 t })
type x = (t:int{ my_predicate t })
это то же самое, что
type y = (t:int{ my_predicate2 t })
X
?
s
constant propext {a b : Prop} : (a ↔ b) → a = b
X
так, что система будет понимать, что это именно тип один, а не условия тождественны
BV
Я как инженер вспоминая свой вуз полностью с тобой согласен
X
вывод (prop1 ==> prop2) тут тоже есть)
X
да правы вы, правы
X
кстати, как там с IDE?
X
в Lean?
s
VS Code с языковым сервером.
X
фух слава богу
s
Работает очень хорошо.
X
к emacs оч тяжело привыкать
s
Кстати, я сильно расширил методичку по пруфам. Там полным-полно примеров на lean.