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

    Комментарии (7) 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» (высокого и низкого).
          Ответить

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