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

0

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
  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 CHayT, (Updated )

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

  • ava CHayT # Ссылка на оригинал 0

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

    • ava CHayT # Ссылка на оригинал 0 ⇈

      Такая вот мята:
      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 Fike # Ссылка на оригинал 0 ⇈

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

          • ava Fike # Ссылка на оригинал 0 ⇈

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

            • ava 3EHuTHblu_nemyx # Ссылка на оригинал 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 # Ссылка на оригинал 0 ⇈

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

                • ava 3EHuTHblu_nemyx # Ссылка на оригинал 0 ⇈

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

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

Помни, guest, за тобой могут следить!

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

    ↑
    8
    ↓