- 1
- 2
- 3
- 4
- 5
- 6
Lemma use_prop_equality : forall {X} (f : X -> Prop) a b,
a = b -> f a -> f b.
Proof.
intros X f a b He Ha.
destruct He. apply Ha.
Qed.
Нашли или выдавили из себя код, который нельзя назвать нормальным, на который без улыбки не взглянешь? Не торопитесь его удалять или рефакторить, — запостите его на говнокод.ру, посмеёмся вместе!
+2
Lemma use_prop_equality : forall {X} (f : X -> Prop) a b,
a = b -> f a -> f b.
Proof.
intros X f a b He Ha.
destruct He. apply Ha.
Qed.
Тактика rewrite не нужна.
j123123 16.08.2017 17:28 # 0
subaru 16.08.2017 17:56 # 0
roman-kashitsyn 16.08.2017 19:24 # +1
К слову, вот более полезная лемма
solnze_dar 12.12.2018 19:49 # 0
roman-kashitsyn 16.08.2017 21:33 # +1
@CHayT, ты используешь шрифт с лигатурами?
CHayT 16.08.2017 21:54 # 0
inkanus-gray 20.08.2017 20:05 # +2
inkanus-gray 20.08.2017 20:09 # 0
roman-kashitsyn 20.08.2017 23:38 # +2
Умляуты тоже занятные: они произошли от дифтонгов ae, oe, ue, в которых e постепенно уехал вверх букв. В средневековых шрифтах e выглядела очень похоже на n, и в итоге стала двумя чёрточками. Форма с e полностью эквивалентна форме с умляутами и встречается довольно часто (например, при использовании анскильного шрифта без умляутов).
В Германии практически не встречаются слова, в которых e следует за буквой с умляутом (потому что если раскрыть умляют, будет две e подряд, некрасиво, это как о писать после ё). А вот в Швейцарии таких полно, например, в именах собственных: Üetliberg, к примеру. Когда их пишут без умляутов, дополнительную е вроде бы не добавляют.
inkanus-gray 21.08.2017 01:36 # 0
Или я плохо искал?
roman-kashitsyn 21.08.2017 15:01 # +1
Это тоже дифтонг, он соответствует в точности тому же звуку, что и -eu- и произносится как "ой". Он обычно появляется при склонении слов, которые содержат -au- (e.g. laufen -> läuft).
То, что гласные рядом с умляутами не стоят – это логично, сложно же такое произносить.
inkanus-gray 21.08.2017 15:14 # −1
https://de.wiktionary.org/wiki/Koeffizient
Произнося это слово, немец должен споткнуться два раза.
roman-kashitsyn 22.08.2017 12:12 # −1
Не более, чем в русском. "Baum" звучит практически так же, как "баум".
> заморский «тротуар»
В немецком тоже есть куча исключений в произношении заимствованных слов (Portemonnaie)
inkanus-gray 22.08.2017 14:14 # 0
В русском «ау» образует два слога, в немецком «au» образует один слог. Это важно для стихотворений.
> В немецком тоже есть куча исключений
Особенно неприятно, когда в одном предложении встречается английское Sweatshirt и французское Portemonnaie. Приходится ломать парсер на каждом слове.