- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
Lemma mint_head_eq CR1 CR2 (te : TE) l m r (t t' : list TE) :
MInt CR1 (l, m, r) (te :: t) ->
MInt CR2 (l, m, r) t' ->
exists t'', t' = te :: t''.
Proof.
intros H1 H2.
inversion_ H1; inversion_ H2; (* generates 25 goals *)
match goal with
|- (exists _, te :: ?T = te :: _) => now exists T
end.
Qed.
Follow us!
Несколько лет назад я прочитал в книге Похлёбкина, что некоторые финно-угорские народы (карелы, коми всякие) употребляют в пищу квашеную рыбу и что находиться в помещении, когда употребляют эту рыбу, неподготовленному человеку невозможно (от запаха можно вырубиться).
Оказывается, шведы эту дрянь у финно-угров переняли... Я думал, это говно давно засыпало песками истории.
типа нычка на чёрный день
если конечно это не байка
странно, что шведы ещё не догадались
Снаут пришел на собеседование к гесту8
разве не надо в начале каждой программы писать «<?php» ?
Вчера как раз в соседнем треде пришли к выводу, что несколько тестов-примеров таки стоит написать, чтобы убедиться, что мы доказываем что-то более-менее относящееся к задуманному, а не тупо мусор.
– Я формально доказал её на кокоидрисе!
– Хорошо, теперь перепиши как чистую любовь на С++ и покрой тестами
– Это не лучший язык для! (хватает тросточку и цилиндр и хохоча убегает)
а иногда без пруфа?)) no warranty