G
Туториал F* мозги основательно так дробит
Size: a a a
2020 June 24
DF
Мне кажется он примерно на это расчитан
G
Знаете как в решениях некоторых задач решение появляется как кролик из шляпы фокусника?
G
Также они верификацию F* показывают
AZ
Знаете как в решениях некоторых задач решение появляется как кролик из шляпы фокусника?
не так
G
А дядя Бреди все разжевывает
AZ
Верификация на F*
G
+++
DF
Кек
AZ
+++
не хочешь мне помочь?
G
А что такое?
AZ
нужно доказать такую штуку:
setWithoutElementIsSet : DecEq a => {xs : Vect _ a} -> {prf : Elem elm xs} -> Set xs -> Set (removeElem_auto elm xs {prf})AZ
я пару часов уже просидел и чет не могу дотумкать
G
Хорошо, домой приду, потыкаю
G
Кто объяснит какой смысл использовать is, not, isnt вместо ==, !, != ?
G
В Си, например
AZ
AZ
я вопроса не понял
G
define is ==