1. Куча / Говнокод #23262

    +2

    1. 1
    2. 2
    3. 3
    4. 4
    5. 5
    6. 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.

    Тактика rewrite не нужна.

    Запостил: CHayT, 12 Августа 2017

    Комментарии (14) RSS

    • Логика первого порядка, ммм...
      Ответить
    • Портировал на Idris
      use_prop_equality : {f: Type -> Type} -> a = b -> f a -> f b
      use_prop_equality Refl n = n

      К слову, вот более полезная лемма
      cong : {f : Type -> Type} -> a = b -> f a = f b
      cong Refl = Refl
      Ответить
    • Раз уж зашла речь об инопланетных технологиях...
      @CHayT, ты используешь шрифт с лигатурами?
      Ответить
      • Вот про такое извращение слышу впервые.
        Ответить
        • А я про это извращение узнал, когда начал изучать TeX. В муриканских и в британских книжках сочетания букв fi, ffi, fl, ffl, ft, fft заменяют лигатурой, из-за чего они читаются ещё хуже.
          Ответить
        • Кстати, говорят, что немецкая буква «эсцет» возникла как лигатура двух готических написаний буквы «s» (высокого и низкого).
          Ответить
          • Мне больше понравилась история происхождения & от слияния e и t. Кстати, есть шрифт, состоящий из одних амперсандтов http://www.typesociety.org/fontaid/iv/.

            Умляуты тоже занятные: они произошли от дифтонгов ae, oe, ue, в которых e постепенно уехал вверх букв. В средневековых шрифтах e выглядела очень похоже на n, и в итоге стала двумя чёрточками. Форма с e полностью эквивалентна форме с умляутами и встречается довольно часто (например, при использовании анскильного шрифта без умляутов).

            В Германии практически не встречаются слова, в которых e следует за буквой с умляутом (потому что если раскрыть умляют, будет две e подряд, некрасиво, это как о писать после ё). А вот в Швейцарии таких полно, например, в именах собственных: Üetliberg, к примеру. Когда их пишут без умляутов, дополнительную е вроде бы не добавляют.
            Ответить
            • Я вообще из сочетаний умляутов с гласными в немецком сходу могу вспомнить только -äu-. Ну, может быть, ещё -äi- где-нибудь встречается. Даже удвоенные умляуты (ää, öö, üü) можно встретить, пожалуй, только в описании деревенских швейцарских диалектов. Ну не любят умляуты в немецком стоять рядом с другими гласными.

              Или я плохо искал?
              Ответить
              • > -äu-

                Это тоже дифтонг, он соответствует в точности тому же звуку, что и -eu- и произносится как "ой". Он обычно появляется при склонении слов, которые содержат -au- (e.g. laufen -> läuft).
                То, что гласные рядом с умляутами не стоят – это логично, сложно же такое произносить.
                Ответить
                • В немецком вообще мало допустимых сочетаний гласных (au, ei, eu — это дифтонги). Это русский язык с лёгкостью проглотил и заморский «тротуар», и заморский «шлагбаум». Хотя иногда бывают и неожиданности:
                  https://de.wiktionary.org/wiki/Koeffizient

                  Произнося это слово, немец должен споткнуться два раза.
                  Ответить
                  • > au — это дифтонг

                    Не более, чем в русском. "Baum" звучит практически так же, как "баум".

                    > заморский «тротуар»

                    В немецком тоже есть куча исключений в произношении заимствованных слов (Portemonnaie)
                    Ответить
                    • > Не более, чем в русском.

                      В русском «ау» образует два слога, в немецком «au» образует один слог. Это важно для стихотворений.

                      > В немецком тоже есть куча исключений

                      Особенно неприятно, когда в одном предложении встречается английское Sweatshirt и французское Portemonnaie. Приходится ломать парсер на каждом слове.
                      Ответить

    Добавить комментарий