couple of questions

1. Coq.
Theorem get_rid_of_stupidity: forall (X:Type) (x y: X), (forall (z: X), x = z -> y = z) -> x = y.

Update:

Theorem get_rid_of_stupidity: forall (X:Type) (x y: X), (forall (z: X), x = z -> y = z) -> x = y.
Proof. 
  intros.
  symmetry.
  apply H.
  reflexivity.
Qed.

2. Go.
I heard there are types, but no generics. So, to get the length of a list (just asking, I don't know what length is good for), should I write a special method for ints, for chars, for strings, for the Animals_Belonging_to_the_Emperor?

хорошо пишут

http://auvasilev.livejournal.com/1241714.html

Stift Melk

научный коммунизм

Ехал на велике, думал, хм, а какие там есть постулаты? С какого это все бодуна? Так смутно-то помнится (в марксизме каждой твари по три); решил полистать интернеты. На вики как-то кратко и неразборчиво. Вот самый разборчивый текст: http://dic.academic.ru/dic.nsf/enc_philosophy/4564/%D0%9D%D0%90%D0%A3%D0%A7%D0%9D%D0%AB%D0%99

Ну так понял, что это все бред на уровне сектантства, бессмысленный поток сложный предложений. Ну примерно как у Маркса в Капитале. К краткому изложению не сводится, потому что контента-то нету. В этом смысле евангелие куда как покруче будет. А это - чистая бессмыслица. Как мы это сдавали? Хз.

мы жили в этих башенках наверху.

Писательница нам сдала свою собственную квартиру, пока ездила куда-то.

жалоба

Coq. Теоремы. Затрахался. Идет как зуб мудрости. Каждая. В этой главе еще 300 с лишним строк примеров.