gds 26.03.2013 14:20 umodniF003ED55

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

coq, говно
#tsezso
re 6 comments !recommend ~bookmark Ssubscribe
1. clayrat 26.03.2013 18:20

полистал слайды Adam Chlipala, "Parametric Higher-Order Abstract Syntax for Mechanized Semantics", но нихуя не понял
какие то тяжелые совсем наркотики этот ваш коq, агду чтоли поучить

#tsezso/1
rereply
2. gds → clayrat /1 26.03.2013 19:06

там не лучше. Примерно однохуйственно.
Но, кажись, за эти часы я кое-что понял. Не ответ, но путь.

#tsezso/2
rereply
3. gds → clayrat /1 26.03.2013 19:07

но в агде заебёшься что-то серьёзное делать.

#tsezso/3
rereply
4. ulidtko → gds /3 26.03.2013 19:41

> упердоливание в типы
> что-то серьёзное

#tsezso/4
rereply
5. gds → ulidtko /4 26.03.2013 20:48

шёл бы ты отсюда, петушок.

#tsezso/5
rereply
6. ulidtko → gds /5 26.03.2013 23:41

пок-пок

#tsezso/6
rereply
Do you really want to delete ?