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

    • ava CHayT 04.08.2021 21:43 # 0

      Когда проще запилить свой dependent pattern matching без блекджека, чем юзать inversion.
      Ответить

    • ava bormand 04.08.2021 21:48 # +1

      Разрушительная мята.
      Ответить

      • ava CHayT 04.08.2021 22:55 # +1

        Такая вот мята:
        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!
        Ответить

    • ava Desktop 04.08.2021 21:50 # 0

      Ваш код вызывает ковид
      Ответить

      • ava CHayT 04.08.2021 22:02 # 0

        Бан в гугле этому теоретику заговора.
        Ответить

      • ava Fike 05.08.2021 10:18 # +3

        Неизвестный whistleblower выложил исходный код программы биоробота «Билл Гейтс» на неприметном сайте «говнокод».
        Ответить

        • ava Desktop 05.08.2021 10:37 # +1

          Bill 5Gates
          Ответить

          • ava 1024-- 05.08.2021 16:30 # +2 

            "Bill Gates"[5] == "G"
            Ответить

            • ava Fike 05.08.2021 19:55 # 0

              Видите? Видите? И после этого вы собираетесь продолжать не верить?
              Ответить

            • ava Desktop 05.08.2021 21:14 # 0

              паскаль не согласен
              Ответить

              • ava 3EHuTHblu_nemyx 05.08.2021 21:20 # 0

                Да, кстати, там символы нумеруются с единицы, нулевой элемент зарезервирован для длины строки.

                Хотя можно задать 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
                Ответить

                • ava Desktop 05.08.2021 21:44 # +2

                  а всё потому, что поколения программистов были испорчены сижкой
                  Ответить

                  • ava 3EHuTHblu_nemyx 05.08.2021 21:47 # +1

                    Вспомнил анекдот про программиста. Приехал программист с женой на вокзал. Жена:
                    –— Посторожи сумки, а я схожу за билетами. Запомни: у нас четыре сумки.
                    Только она отошла, слышит крик мужа:
                    —– Кто украл сумку?
                    Жена:
                    –— Что ты кричишь, у нас же всё на месте.
                    Он:
                    —– Ну вот сама посчитай: ноль, один, два, три.
                    Ответить

    • ava nycpblcmuk 05.08.2021 09:42 # +1

      Пуфыстик ничего не понимает. Переведи на «PHP».
      Ответить

      • ava bormand 05.08.2021 09:51 # 0

        @
        Ответить

        • ava nycpblcmuk 05.08.2021 09:52 # +2

          Пуфыстик благодарит тебя. Значит, этот код ничего не выводит?
          Ответить

      • ava CHayT 05.08.2021 11:31 # +2

        Для этого надо extraction в PHP пилить, как нибудь потом.
        Ответить

      • ava 1024-- 05.08.2021 16:32 # +2

        Присоединяюсь. Для меня, чуть укушенного сишкой, из всего кода читается только signed middle int.
        Ответить

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