DM
прости что помогаю увеличивать гору
Size: a a a
2020 April 02
AT
прости что помогаю увеличивать гору
Ну, у тебя сова на аватаре. А мы, птицы, должны вместе держаться
KS
@dmsol извините, у вас спринг протек
AT
главпетух -- это конкретный человек, сейчас это Matthieu Sozeau
AT
а какие задачки интересуют?
AT
в Software Foundations много задачек
я для курсов своих тоже какое-то количество выкладываю
я для курсов своих тоже какое-то количество выкладываю
AD
где то был большой задачник
w
где то был большой задачник
AT
в Software Foundations много задачек
я для курсов своих тоже какое-то количество выкладываю
я для курсов своих тоже какое-то количество выкладываю
- на codewars есть ката по Coq
- https://exercism.io/tracks/coq (но не смотрел сам)
- https://web.mit.edu/~jgross/Public/coq/Exercises.v
- https://osa1.net/posts/2014-07-12-fun-coq-exercises.html
- https://jamesrwilcox.com/InductionExercises.html
- https://verifcomp.dbp.io
- https://exercism.io/tracks/coq (но не смотрел сам)
- https://web.mit.edu/~jgross/Public/coq/Exercises.v
- https://osa1.net/posts/2014-07-12-fun-coq-exercises.html
- https://jamesrwilcox.com/InductionExercises.html
- https://verifcomp.dbp.io
KS
Ого, Каюшка в тофу коньтрибутит
DM
в Software Foundations много задачек
я для курсов своих тоже какое-то количество выкладываю
я для курсов своих тоже какое-то количество выкладываю
а под тлю?
видел репу с доказательством только
видел репу с доказательством только
AT
а под тлю?
видел репу с доказательством только
видел репу с доказательством только
задачек не видел, вот есть репа с примерами -- https://github.com/tlaplus/Examples
AT
их там, страшно сказать, 69 (!)
A
Kirill Shelopugin
Ого, Каюшка в тофу коньтрибутит
> naive LEGACY syntax encodings
DM
их там, страшно сказать, 69 (!)
не православно, нужно еще один добавить
AT
не православно, нужно еще один добавить
или 36 убавить