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

    +1

    1. 01
    2. 02
    3. 03
    4. 04
    5. 05
    6. 06
    7. 07
    8. 08
    9. 09
    10. 10
    11. 11
    12. 12
    13. 13
    14. 14
    15. 15
    16. 16
    17. 17
    18. 18
    19. 19
    20. 20
    21. 21
    Ltac destruct_mint_ H := 
       match type of H with
          (MInt_ _ ?z ?t) =>
          lazymatch goal with
            |- ?GOAL =>
            refine (match H in (MInt_ _ z0 t0) return (z = z0 -> t = t0 -> GOAL) with
                    | mint_nil    _  =>
                      fun Heq_z Heq_tt_ =>
                        ltac:(destruct_mint_common Heq_tt_ Heq_z H)
                    | mint_cons   _ te rest l      r   t H =>
                      fun Heq_z Heq_tt_ =>
                        ltac:(destruct_mint_common Heq_tt_ Heq_z H)
                    | mint_cons_l _ te rest l r z t Hz H  =>
                      fun Heq_z Heq_tt_ =>
                        ltac:(destruct_mint_common Heq_tt_ Heq_z H)
                    | mint_cons_r _ te te' rest l r z t Hz Hcomm H =>
                      fun Heq_z Heq_tt_ =>
                        ltac:(destruct_mint_common Heq_tt_ Heq_z H)
                    end (eq_refl z) (eq_refl t))
          end
        end.

    Наебавшись с inversion в механизированным доказательстве, закрыл я очи.

    Запостил: CHayT, 04 Августа 2021

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

    • Когда проще запилить свой dependent pattern matching без блекджека, чем юзать inversion.
      Ответить
    • Разрушительная мята.
      Ответить
      • Такая вот мята:
        Inductive MInt_ : Traces -> @TraceEnsemble TE :=
            | mint_nil :
                MInt_ ([], None, []) []
            | mint_cons : forall te rest l r t,
                MInt_ (l, clean rest, r) t ->
                MInt_ (l, Some (te :: rest), r) (te :: t)
            | mint_cons_l : forall te rest l r zipper t,
                zipper >z (l, clean rest, r) ->
                MInt_ zipper t ->
                MInt_ (l, Some (te :: rest), r) (te :: t)
            | mint_cons_r : forall te te' rest l r zipper t,
                zipper <z (l, clean rest, r)->
                comm_rel te te' ->
                MInt_ zipper (te' :: t) ->
                MInt_ (l, Some (te :: rest), r) (te :: te' :: t).


        (Multi Interleaving). Тип данных, генерирующий все некоммутирующие исполнения системы. Вроде даже работает, но пиздец некрасиво, конечно.
        Надо чтобы CPS!
        Ответить
    • Ваш код вызывает ковид
      Ответить
      • Бан в гугле этому теоретику заговора.
        Ответить
      • Неизвестный whistleblower выложил исходный код программы биоробота «Билл Гейтс» на неприметном сайте «говнокод».
        Ответить
        • Bill 5Gates
          Ответить
          • "Bill Gates"[5] == "G"
            Ответить
            • Видите? Видите? И после этого вы собираетесь продолжать не верить?
              Ответить
            • паскаль не согласен
              Ответить
              • Да, кстати, там символы нумеруются с единицы, нулевой элемент зарезервирован для длины строки.

                Хотя можно задать array of char с любым диапазоном индексов:
                const
                    _PITUH = 'Bill Gates';
                    pituh: array[0..length(_PITUH)-1]of char = _PITUH;
                begin
                	Writeln(pituh[5])
                end.


                https://ideone.com/rn1Rzy
                Ответить
                • а всё потому, что поколения программистов были испорчены сижкой
                  Ответить
                  • Вспомнил анекдот про программиста. Приехал программист с женой на вокзал. Жена:
                    –— Посторожи сумки, а я схожу за билетами. Запомни: у нас четыре сумки.
                    Только она отошла, слышит крик мужа:
                    —– Кто украл сумку?
                    Жена:
                    –— Что ты кричишь, у нас же всё на месте.
                    Он:
                    —– Ну вот сама посчитай: ноль, один, два, три.
                    Ответить
    • Пуфыстик ничего не понимает. Переведи на «PHP».
      Ответить
      • @
        Ответить
        • Пуфыстик благодарит тебя. Значит, этот код ничего не выводит?
          Ответить
      • Для этого надо extraction в PHP пилить, как нибудь потом.
        Ответить
      • Присоединяюсь. Для меня, чуть укушенного сишкой, из всего кода читается только signed middle int.
        Ответить

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