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

    • ava bormand 06.06.2021 17:28 # 0

      SEO коммент.
      Ответить

    • ava nuTepcKuu_nemyx 06.06.2021 19:31 # 0

      Переведи хоть на «русский». Сегодня день русского языка, кстати.
      Ответить

      • ava Soul_re@ver 06.06.2021 19:35 # +1

        Гугл спешит на помощь!

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

        Цель верна.
        спать 3.
        точный I.
        Qed.
        Ответить

        • ava bormand 06.06.2021 19:45 # +1

          eapply -- эприменить (э - экзистенциально)
          Qed -- ну ч.т.д. же...
          Ответить

      • ava bormand 06.06.2021 19:51 # +2

        Имитация бурной деятельности.

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

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

        • ava j123123 11.06.2021 23:15 # +1

          А нахуя для доказывания какой-либо хрени нужно вообще было добавлять что-то, связанное с учетом времени исполнения этой питушни? Ну т.е. зачем там вообще этот "оператор" timeout добавили?

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

          • ava bormand 11.06.2021 23:23 # 0

            Х.з., там даже в доке написано, что это сомнительный оператор и лучше его не юзать.
            Ответить

          • ava gologub 11.06.2021 23:48 # 0

            небось дококозательство вероятностное, можно ограничить сколько раундов крутить
            Ответить

            • ava bormand 11.06.2021 23:50 # 0

              Да нет, там все детерминированное вроде в стандартных тактиках. Разве что если плагин какой-то прикрутить.
              Ответить

          • ava Hijikata 12.06.2021 16:25 # +1

            мб чтобы можно было какой-то самопальный профайлер для тайпчекера сделать
            Ответить

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