- 1
- 2
- 3
- 4
- 5
- 6
- 7
- 8
- 9
- 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.
CHayT # 0
CHayT # 0 ⇈
defecate-plusplus # 0 ⇈
Mithun_Chakraborty # 0 ⇈
CHayT # 0 ⇈
defecate-plusplus # 0 ⇈
CHayT # 0 ⇈
bormand # 0 ⇈
CHayT # 0 ⇈
Desktop # 0 ⇈
Mithun_Chakraborty # 0 ⇈
Несколько лет назад я прочитал в книге Похлёбкина, что некоторые финно-угорские народы (карелы, коми всякие) употребляют в пищу квашеную рыбу и что находиться в помещении, когда употребляют эту рыбу, неподготовленному человеку невозможно (от запаха можно вырубиться).
Оказывается, шведы эту дрянь у финно-угров переняли... Я думал, это говно давно засыпало песками истории.
Desktop # 0 ⇈
типа нычка на чёрный день
если конечно это не байка
defecate-plusplus # 0 ⇈
странно, что шведы ещё не догадались
Desktop # 0 ⇈
defecate-plusplus # 0 ⇈
Desktop # 0 ⇈
Mithun_Chakraborty # 0
defecate-plusplus # 0 ⇈
Mithun_Chakraborty # 0 ⇈
rotoeb # 0
bormand # 0 ⇈
guest # 0 ⇈
oaoaoammm # 0 ⇈
Снаут пришел на собеседование к гесту8
defecate-plusplus # 0 ⇈
разве не надо в начале каждой программы писать «<?php» ?
oaoaoammm # 0 ⇈
bormand # 0 ⇈
CHayT # 0 ⇈
bormand # 0 ⇈
bormand # 0 ⇈
Вчера как раз в соседнем треде пришли к выводу, что несколько тестов-примеров таки стоит написать, чтобы убедиться, что мы доказываем что-то более-менее относящееся к задуманному, а не тупо мусор.
Desktop # 0 ⇈
– Я формально доказал её на кокоидрисе!
– Хорошо, теперь перепиши как чистую любовь на С++ и покрой тестами
– Это не лучший язык для! (хватает тросточку и цилиндр и хохоча убегает)
bormand # 0 ⇈
Desktop # 0 ⇈
а иногда без пруфа?)) no warranty
CHayT # 0 ⇈