- 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.
CHayT 14.10.2020 00:44 # +1
CHayT 14.10.2020 10:56 # +1
defecate-plusplus 14.10.2020 11:00 # +2
Mithun_Chakraborty 14.10.2020 11:09 # +1
CHayT 14.10.2020 11:13 # +1
defecate-plusplus 14.10.2020 15:37 # 0
CHayT 14.10.2020 15:43 # +1
bormand 14.10.2020 15:43 # 0
CHayT 14.10.2020 15:45 # +2
Desktop 14.10.2020 15:47 # 0
Mithun_Chakraborty 14.10.2020 15:50 # 0
Несколько лет назад я прочитал в книге Похлёбкина, что некоторые финно-угорские народы (карелы, коми всякие) употребляют в пищу квашеную рыбу и что находиться в помещении, когда употребляют эту рыбу, неподготовленному человеку невозможно (от запаха можно вырубиться).
Оказывается, шведы эту дрянь у финно-угров переняли... Я думал, это говно давно засыпало песками истории.
Desktop 14.10.2020 15:54 # 0
типа нычка на чёрный день
если конечно это не байка
defecate-plusplus 14.10.2020 16:08 # +3
странно, что шведы ещё не догадались
Desktop 14.10.2020 16:11 # +1
defecate-plusplus 14.10.2020 16:13 # +4
Desktop 14.10.2020 14:18 # 0
Mithun_Chakraborty 14.10.2020 08:58 # +2
defecate-plusplus 14.10.2020 09:27 # +1
Mithun_Chakraborty 14.10.2020 09:45 # +2
rotoeb 14.10.2020 10:26 # −20
bormand 14.10.2020 10:28 # 0
guest8 14.10.2020 10:35 # −999
oaoaoammm 14.10.2020 13:12 # 0
Снаут пришел на собеседование к гесту8
defecate-plusplus 14.10.2020 13:35 # +3
разве не надо в начале каждой программы писать «<?php» ?
oaoaoammm 14.10.2020 13:50 # −1
bormand 14.10.2020 13:55 # −1
CHayT 14.10.2020 13:56 # −1
bormand 14.10.2020 14:00 # +3
bormand 14.10.2020 14:16 # +1
Вчера как раз в соседнем треде пришли к выводу, что несколько тестов-примеров таки стоит написать, чтобы убедиться, что мы доказываем что-то более-менее относящееся к задуманному, а не тупо мусор.
Desktop 14.10.2020 14:21 # +1
– Я формально доказал её на кокоидрисе!
– Хорошо, теперь перепиши как чистую любовь на С++ и покрой тестами
– Это не лучший язык для! (хватает тросточку и цилиндр и хохоча убегает)
bormand 14.10.2020 14:25 # 0
Desktop 14.10.2020 14:26 # −1
а иногда без пруфа?)) no warranty
CHayT 14.10.2020 14:25 # +1