*coq

Как выяснилось, карго-культ по отношению к PHOAS работает плохо, особенно если нужно делать чуть больше, чем простую лямбду. Чо ж делать-то, а? Может кто-нибудь объяснит потолковее, чем в гуглоте?

#tsezso

6 comments

Зарелизил мелкую библиотечку для отладки редукций выражений в пределах coq: https://bitbucket.org/gds/coq-breakpoint...

#tsszng

6 comments

"
Rc43: What does name of Agda mean?
olahol_: Agda the chicken, swedish floksong
"
Я всегда знал, что Coq — строго над Agda.

#tsszgo

1 comment

Наша редакция рада ответить на просьбу господина @ulidtko, изложенную в http://amd63.psto.net/tsfgse#123 , нижеследующим куском кода: https://gist.github.com/gdsfh/7140f41aca...
Там в каментах я показал, во что экстрактится всё это безобразие. Как обычно, все пруф-термы стёрты, остались только ... more →

#tsiezf

2 comments

"построение термов тактиками в coq — безопасно" [ http://gds.livejournal.com/66182.html ]

#tinhoi

add comment

Coq quick reference: https://wiki.mq.edu.au/display/plrg/Reso...

#tfifzf

add comment

http://www.sendspace.com/file/4vtin4
Запись диалога знакомого в техподдержке с клиентом.

#tfteen

1 comment

Опыт использования Coq на практике, или Как я сам себя отпетушил COQОКОКОКО < http://gds.livejournal.com/65879.html >

#thfgnh

1 comment

$ hg remove ErrorMonad.v StateMonad.v Monads.v Exceptions.v
до свиданья, наш ласковый мишка!11111

#onfhts

9 comments

законтачился о монадные трансформеры, реализовав их (заодно манатки, заодно do-нотацию, заодно доказательства законов монад и трансформеров) в coq.

Fixpoint test1 (lst : list nat)
: idents_state Res MRes (list (nat * S.string))
:=
match lst with
| nil => ret nil
| cons h t =>
match h with
| 0 => lift (throw _ ... more →

#onoiso

add comment

In the Soviet Coq, the monad transformer writes You!

#onotgi

3 comments

сейчас наткнулся на подобную штуку, и немного генерализирую.
при написании веб-сервера на coq обнаружим, что рекурсивная функция, читающая http-заголовки, внезапно потребует доказательства завершимости. По идее, оно должно включить в себя конечность числа символов в прочитанных заголовках, либо конечность как числа ... more →

#osgisi

add comment

I heard Coq like types, so we put type in your type so you can type your types while you are typing your types.

и больше ничего не могу сказать про текущие дела :)

#osgtte

7 comments

ааа, убейте меня, иначе я всё забрызгаю тут1111
@default631">http://flint.cs.yale.edu/cs428/coq/doc/R...
СУТЬ:
У вас есть индуктивный тип данных для представления вашего игрушечного AST, специфичного для вашей предметной области.
У вас есть функция, преобразующая _ваши_ значения из AST в ... more →

#osfnnt

6 comments

true <> false
Неожиданно? Однако, это так.
Эта шокирующая истина теперь конструктивно доказана: http://gds.livejournal.com/63887.html

#osheot

2 comments

http://gds.livejournal.com/63527.html — как обычно, интересуют каменты там либо тут. (не нравится щёлкать на ссылку — не щёлкайте, но копипастить ту простыню сюда я не буду.)

#oshhoh

add comment