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

    • ava j123123 16.08.2017 17:28 # 0

      Логика первого порядка, ммм...
      Ответить

    • ava roman-kashitsyn 16.08.2017 19:24 # +1

      Портировал на 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
      Ответить

    • ava roman-kashitsyn 16.08.2017 21:33 # +1

      Раз уж зашла речь об инопланетных технологиях...
      @CHayT, ты используешь шрифт с лигатурами?
      Ответить

      • ava CHayT 16.08.2017 21:54 # 0

        Вот про такое извращение слышу впервые.
        Ответить

        • ava inkanus-gray 20.08.2017 20:05 # +2

          А я про это извращение узнал, когда начал изучать TeX. В муриканских и в британских книжках сочетания букв fi, ffi, fl, ffl, ft, fft заменяют лигатурой, из-за чего они читаются ещё хуже.
          Ответить

        • ava inkanus-gray 20.08.2017 20:09 # 0

          Кстати, говорят, что немецкая буква «эсцет» возникла как лигатура двух готических написаний буквы «s» (высокого и низкого).
          Ответить

          • ava roman-kashitsyn 20.08.2017 23:38 # +2

            Мне больше понравилась история происхождения & от слияния e и t. Кстати, есть шрифт, состоящий из одних амперсандтов http://www.typesociety.org/fontaid/iv/.

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

            В Германии практически не встречаются слова, в которых e следует за буквой с умляутом (потому что если раскрыть умляют, будет две e подряд, некрасиво, это как о писать после ё). А вот в Швейцарии таких полно, например, в именах собственных: Üetliberg, к примеру. Когда их пишут без умляутов, дополнительную е вроде бы не добавляют.
            Ответить

            • ava inkanus-gray 21.08.2017 01:36 # 0

              Я вообще из сочетаний умляутов с гласными в немецком сходу могу вспомнить только -äu-. Ну, может быть, ещё -äi- где-нибудь встречается. Даже удвоенные умляуты (ää, öö, üü) можно встретить, пожалуй, только в описании деревенских швейцарских диалектов. Ну не любят умляуты в немецком стоять рядом с другими гласными.

              Или я плохо искал?
              Ответить

              • ava roman-kashitsyn 21.08.2017 15:01 # +1

                > -äu-

                Это тоже дифтонг, он соответствует в точности тому же звуку, что и -eu- и произносится как "ой". Он обычно появляется при склонении слов, которые содержат -au- (e.g. laufen -> läuft).
                То, что гласные рядом с умляутами не стоят – это логично, сложно же такое произносить.
                Ответить

                • ava inkanus-gray 21.08.2017 15:14 # −1

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

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

                  • ava roman-kashitsyn 22.08.2017 12:12 # −1

                    > au — это дифтонг

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

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

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

                    • ava inkanus-gray 22.08.2017 14:14 # 0

                      > Не более, чем в русском.

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

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

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

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