Куча говна / Говнокод #27457 Ссылка на оригинал

0

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
Tactic Notation "sleep" integer(seconds) :=
    do seconds try solve [ timeout 1 (repeat eapply proj1) ].

Goal True.
    sleep 3.
    exact I.
Qed.

Какой пруф )))

Запостил: bormand bormand, (Updated )

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

  • Переведи хоть на «русский». Сегодня день русского языка, кстати.
    Ответить
    • Гугл спешит на помощь!

      Тактическое обозначение "сна" целое число (секунды): =
      сделать секунды попробуйте решить [тайм-аут 1 (повторить eapply proj1)].

      Цель верна.
      спать 3.
      точный I.
      Qed.
      Ответить
      • eapply -- эприменить (э - экзистенциально)
        Qed -- ну ч.т.д. же...
        Ответить
    • Имитация бурной деятельности.

      Ставим себе целью доказать True. Применяем к нему теорему A /\ B -> A (proj1) пока не заебёт пройдёт секунда. Повторяем для верности три раза. Затем, как ни в чём не бывало, доказываем True с помощью его единственного конструктора I.

      З.Ы. Интересно, а что будет, если комп слишком быстрый и за секунду сожрет всю память. Формула ведь растёт: True, True /\ B, (True /\ B) /\ B ...
      Ответить
      • А нахуя для доказывания какой-либо хрени нужно вообще было добавлять что-то, связанное с учетом времени исполнения этой питушни? Ну т.е. зачем там вообще этот "оператор" timeout добавили?

        Допустим, один процессор быстрее другого, за одну секунду больше всякой питушни понаприменяет и может из-за этого доказать некую хуйню, а другой за одну секунду чего-то не успеет, и получится так, что на одном процессоре питушня доказывается, а на другой нет? И нахуя такое надо?
        Ответить
        • Х.з., там даже в доке написано, что это сомнительный оператор и лучше его не юзать.
          Ответить
        • небось дококозательство вероятностное, можно ограничить сколько раундов крутить
          Ответить
          • Да нет, там все детерминированное вроде в стандартных тактиках. Разве что если плагин какой-то прикрутить.
            Ответить
        • мб чтобы можно было какой-то самопальный профайлер для тайпчекера сделать
          Ответить

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

Переведи на "PHP", guest!

    А не использовать ли нам bbcode?


    8