|
Anton Trunov
@
falsenov
Saint Petersburg
|
|
Coq programmer at @zilliqa; previously at @IMDEA_Software
|
|
|
71
Tweetovi
|
255
Pratim
|
263
Osobe koje vas prate
|
| Tweetovi |
| Anton Trunov proslijedio/la je tweet | ||
|
The Coq proof assistant
@CoqLang
|
27. sij |
|
Hello all! Welcome to Coq's official Twitter!
We will share exciting news and events related to Coq; see github.com/coq/coq for the proper channels for bug reports or technical discussion.
This account is community-managed by @ejgallego, @falsenov, and @Zimm_i48. Have fun!
|
||
|
||
|
|
Anton Trunov
@falsenov
|
24. sij |
|
You might like some more vanilla intro-patterns then :)
Not as powerful as the SSReflect patterns, but still can be combined in a not-so-trivial way, e.g. intros [=->%length_zero_iff_nil].
A couple examples and explanations are here github.com/tchajed/coq-tr…
|
||
|
|
||
|
|
Anton Trunov
@falsenov
|
24. sij |
|
My solution takes 61 chars not including Qed. and indentation: stackoverflow.com/questions/1674…
|
||
|
|
||
|
|
Anton Trunov
@falsenov
|
23. sij |
|
It's a bit more tricky than that ;)
|
||
|
|
||
|
|
Anton Trunov
@falsenov
|
7. sij |
|
I also like this post by Joachim Breitner explaining this: joachim-breitner.de/blog/732-Isabe…
|
||
|
|
||
|
|
Anton Trunov
@falsenov
|
5. sij |
|
коммутирует, но только если перемещаешься на работу и обратно домой всеми указанными способами ;)
|
||
|
|
||
|
|
Anton Trunov
@falsenov
|
5. sij |
|
There are some katas for Agda/Coq/Idris on codewars.com
|
||
|
|
||
|
|
Anton Trunov
@falsenov
|
30. pro |
|
спасибо большое за интерес! отвечу на почту :)
|
||
|
|
||
|
|
Anton Trunov
@falsenov
|
28. pro |
|
у меня несколько вариантов для перевода wildcard: 1) палочка-выручалочка (или просто выручалочка), 2) волшебная палочка, 3) (неоткалиброванный) умклайдет
|
||
|
|
||
|
|
Anton Trunov
@falsenov
|
27. pro |
|
спасибо, я передам :)
|
||
|
|
||
|
|
Anton Trunov
@falsenov
|
27. pro |
|
Еще не все лекции смонтированы и названия на youtube не подправлены -- я правил пока только на edu.tinkoff.ru (но курс там приватный).
|
||
|
|
||
|
|
Anton Trunov
@falsenov
|
27. pro |
|
Спасибо огромнейшее, Олег! Хочу также поблагодарить Евгения Ивашкевича, без которого этот курс не состоялся бы; компанию Zilliqa Research и лично Амрита Кумара за поддержку этого начинания. А еще у меня была лучшая аудитория в мире!
|
||
|
|
||
|
|
Anton Trunov
@falsenov
|
14. pro |
|
|
||
|
|
Anton Trunov
@falsenov
|
13. pro |
|
Congrats on your successful defense! Great work!
|
||
|
|
||
|
|
Anton Trunov
@falsenov
|
24. lis |
|
|
||
| Anton Trunov proslijedio/la je tweet | ||
|
Zilliqa
@zilliqa
|
24. lis |
|
Yes we did it! We won the Distinguished Artifact Award at OOPSLA 2019 @splashcon. Thanks to all the hard work of the team and the support of all of you for making this possible. It's all about safer smart contract programming with #Scilla!
#PushReuseableCode 🔥 pic.twitter.com/vKyIorVvhj
|
||
|
|
||
|
|
Anton Trunov
@falsenov
|
4. lis |
|
Ой, я не ведая 😊
|
||
|
|
||
| Anton Trunov proslijedio/la je tweet | ||
|
Mike Potanin
@MikePotanin
|
4. lis |
|
github.com/anton-trunov/c…
Очень интересные задачи в домашках и семинарах. Рекомендую порешать даже тем, кто не ходит на курс.
Приходится поломать голову даже с ванильным Coq. А уж с ssreflect...
|
||
|
|
||
|
|
Anton Trunov
@falsenov
|
1. lis |
|
github.com/math-comp/math… - здесь кое-что можно найти
|
||
|
|
||
|
|
Anton Trunov
@falsenov
|
27. ruj |
|
Гольфить! Но так, чтобы одна строчка формального док-ва соответствовала одному предложению неформального.
|
||
|
|
||