Обсуждали изготовление домашнего кваса, опубликую личный рецепт.
( Read more... )

ответ на очередное тупопёздничество этой леди, на этот раз тут: http://nicka-startcev.livejournal.com/1651259.html?thread=5538875#t5538875Read more... )

Решил вынести ответ на камент в отдельный пост. Так как дело было в жыжыцэ, пост будет тоже жэжэшный ( Read more... )

Взял несложную (как казалось) задачку, потыкал в неё палочкой, отчаялся, дошёл до #coq irc, изложил проблему, но не помогли. Зато теперь есть изложение этой проблемы:
( Read more... )

Кое в чём разобрался, близко к прошлой проблеме.
А вы посмотрите, правильно ли.

Definition true_neq_false
: true <> false
( Read more... )

Решил вспомнить молодость и подоказывать кое-что. У известного Адама взял какой-то пример, который он доказывает через свою придуманную для книги CPDT тактику "crush", но мне это не нравится. Хотя бы тем, что тактики не нравятся. Я хочу что-то более приближённое к конструктивному построению доказательства ( Read more... )

(как бы разворачивая каменты из предыдущего поста ( Read more... )

Data.VecN в окамле: https://bitbucket.org/gds/vecn/src
И, чорт возми, опять зависимые типы не пригодились. Да что за беда...

Одна из частей моего интернет-общения с людьми состоит в том, что я шлю одинаковые/похожие сообщения по жабберу нескольким людям одновременно ( Read more... )

А теперь -- о тупой практике вопрос ( Read more... )