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

    +4

    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, 06 Июня 2021

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

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

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

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

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

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

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

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