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)
  2. Куча / Говнокод #27545

    0

    1. 1
    Пиздец-оффтоп #26

    #1: https://govnokod.ru/26503 https://govnokod.xyz/_26503
    #2: https://govnokod.ru/26541 https://govnokod.xyz/_26541
    #3: https://govnokod.ru/26583 https://govnokod.xyz/_26583
    #4: https://govnokod.ru/26689 https://govnokod.xyz/_26689
    #5: https://govnokod.ru/26784 https://govnokod.xyz/_26784
    #5: https://govnokod.ru/26839 https://govnokod.xyz/_26839
    #6: https://govnokod.ru/26986 https://govnokod.xyz/_26986
    #7: https://govnokod.ru/27007 https://govnokod.xyz/_27007
    #8: https://govnokod.ru/27023 https://govnokod.xyz/_27023
    #9: https://govnokod.ru/27098 https://govnokod.xyz/_27098
    #10: https://govnokod.ru/27125 https://govnokod.xyz/_27125
    #11: https://govnokod.ru/27129 https://govnokod.xyz/_27129
    #12: https://govnokod.ru/27184 https://govnokod.xyz/_27184
    #13: https://govnokod.ru/27286 https://govnokod.xyz/_27286
    #14: https://govnokod.ru/27298 https://govnokod.xyz/_27298
    #15: https://govnokod.ru/27322 https://govnokod.xyz/_27322
    #16: https://govnokod.ru/27328 https://govnokod.xyz/_27328
    #17: https://govnokod.ru/27346 https://govnokod.xyz/_27346
    #18: https://govnokod.ru/27374 https://govnokod.xyz/_27374
    #19: https://govnokod.ru/27468 https://govnokod.xyz/_27468
    #20: https://govnokod.ru/27469 https://govnokod.xyz/_27469
    #21: https://govnokod.ru/27479 https://govnokod.xyz/_27479
    #22: https://govnokod.ru/27485 https://govnokod.xyz/_27485
    #23: https://govnokod.ru/27493 https://govnokod.xyz/_27493
    #24: https://govnokod.ru/27501 https://govnokod.xyz/_27501
    #25: https://govnokod.ru/27521 https://govnokod.xyz/_27521

    nepeKamHblu_nemyx, 02 Августа 2021

    Комментарии (2940)
  3. Куча / Говнокод #27544

    0

    1. 1
    IT Оффтоп #105

    #75: https://govnokod.ru/27166 https://govnokod.xyz/_27166
    #76: https://govnokod.ru/27168 https://govnokod.xyz/_27168
    #77: https://govnokod.ru/27186 https://govnokod.xyz/_27186
    #78: https://govnokod.ru/27219 https://govnokod.xyz/_27219
    #79: https://govnokod.ru/27254 https://govnokod.xyz/_27254
    #80: https://govnokod.ru/27270 https://govnokod.xyz/_27270
    #81: https://govnokod.ru/27280 https://govnokod.xyz/_27280
    #82: https://govnokod.ru/27284 https://govnokod.xyz/_27284
    #83: https://govnokod.ru/27296 https://govnokod.xyz/_27296
    #84: https://govnokod.ru/27336 https://govnokod.xyz/_27336
    #85: https://govnokod.ru/27381 https://govnokod.xyz/_27381
    #86: https://govnokod.ru/27405 https://govnokod.xyz/_27405
    #87: https://govnokod.ru/27429 https://govnokod.xyz/_27429
    #88: https://govnokod.ru/27432 https://govnokod.xyz/_27432
    #89: https://govnokod.ru/27435 https://govnokod.xyz/_27435
    #90: https://govnokod.ru/27439 https://govnokod.xyz/_27439
    #91: https://govnokod.ru/27449 https://govnokod.xyz/_27449
    #92: https://govnokod.ru/27460 https://govnokod.xyz/_27460
    #93: https://govnokod.ru/27463 https://govnokod.xyz/_27463
    #94: https://govnokod.ru/27466 https://govnokod.xyz/_27466
    #95: https://govnokod.ru/27473 https://govnokod.xyz/_27473
    #96: https://govnokod.ru/27478 https://govnokod.xyz/_27478
    #97: https://govnokod.ru/27484 https://govnokod.xyz/_27484
    #98: https://govnokod.ru/27495 https://govnokod.xyz/_27495
    #99: https://govnokod.ru/27504 https://govnokod.xyz/_27504
    #100: https://govnokod.ru/27508 https://govnokod.xyz/_27508
    #101: https://govnokod.ru/27511 https://govnokod.xyz/_27511
    #102: https://govnokod.ru/27518 https://govnokod.xyz/_27518
    #103: https://govnokod.ru/27526 https://govnokod.xyz/_27526
    #104: https://govnokod.ru/27534 https://govnokod.xyz/_27534

    nepeKamHblu_nemyx, 01 Августа 2021

    Комментарии (2460)
  4. Куча / Говнокод #-27539

    +1

    1. 1
    Именно поэтому я за «PHP» #4

    #1: https://govnokod.ru/26462 https://govnokod.xyz/_26462
    #2: https://govnokod.ru/26827 https://govnokod.xyz/_26827
    #3: https://govnokod.ru/26832 https://govnokod.xyz/_26832

    nepeKamHblu_nemyx, 28 Июля 2021

    Комментарии (9875)
  5. Куча / Говнокод #27534

    0

    1. 1
    IT Оффтоп #104

    #74: https://govnokod.ru/27160 https://govnokod.xyz/_27160
    #75: https://govnokod.ru/27166 https://govnokod.xyz/_27166
    #76: https://govnokod.ru/27168 https://govnokod.xyz/_27168
    #77: https://govnokod.ru/27186 https://govnokod.xyz/_27186
    #78: https://govnokod.ru/27219 https://govnokod.xyz/_27219
    #79: https://govnokod.ru/27254 https://govnokod.xyz/_27254
    #80: https://govnokod.ru/27270 https://govnokod.xyz/_27270
    #81: https://govnokod.ru/27280 https://govnokod.xyz/_27280
    #82: https://govnokod.ru/27284 https://govnokod.xyz/_27284
    #83: https://govnokod.ru/27296 https://govnokod.xyz/_27296
    #84: https://govnokod.ru/27336 https://govnokod.xyz/_27336
    #85: https://govnokod.ru/27381 https://govnokod.xyz/_27381
    #86: https://govnokod.ru/27405 https://govnokod.xyz/_27405
    #87: https://govnokod.ru/27429 https://govnokod.xyz/_27429
    #88: https://govnokod.ru/27432 https://govnokod.xyz/_27432
    #89: https://govnokod.ru/27435 https://govnokod.xyz/_27435
    #90: https://govnokod.ru/27439 https://govnokod.xyz/_27439
    #91: https://govnokod.ru/27449 https://govnokod.xyz/_27449
    #92: https://govnokod.ru/27460 https://govnokod.xyz/_27460
    #93: https://govnokod.ru/27463 https://govnokod.xyz/_27463
    #94: https://govnokod.ru/27466 https://govnokod.xyz/_27466
    #95: https://govnokod.ru/27473 https://govnokod.xyz/_27473
    #96: https://govnokod.ru/27478 https://govnokod.xyz/_27478
    #97: https://govnokod.ru/27484 https://govnokod.xyz/_27484
    #98: https://govnokod.ru/27495 https://govnokod.xyz/_27495
    #99: https://govnokod.ru/27504 https://govnokod.xyz/_27504
    #100: https://govnokod.ru/27508 https://govnokod.xyz/_27508
    #101: https://govnokod.ru/27511 https://govnokod.xyz/_27511
    #102: https://govnokod.ru/27518 https://govnokod.xyz/_27518
    #103: https://govnokod.ru/27526 https://govnokod.xyz/_27526

    nepeKamHblu_nemyx, 23 Июля 2021

    Комментарии (2039)
  6. Куча / Говнокод #27526

    0

    1. 1
    IT Оффтоп #103

    #73: https://govnokod.ru/27136 https://govnokod.xyz/_27136
    #74: https://govnokod.ru/27160 https://govnokod.xyz/_27160
    #75: https://govnokod.ru/27166 https://govnokod.xyz/_27166
    #76: https://govnokod.ru/27168 https://govnokod.xyz/_27168
    #77: https://govnokod.ru/27186 https://govnokod.xyz/_27186
    #78: https://govnokod.ru/27219 https://govnokod.xyz/_27219
    #79: https://govnokod.ru/27254 https://govnokod.xyz/_27254
    #80: https://govnokod.ru/27270 https://govnokod.xyz/_27270
    #81: https://govnokod.ru/27280 https://govnokod.xyz/_27280
    #82: https://govnokod.ru/27284 https://govnokod.xyz/_27284
    #83: https://govnokod.ru/27296 https://govnokod.xyz/_27296
    #84: https://govnokod.ru/27336 https://govnokod.xyz/_27336
    #85: https://govnokod.ru/27381 https://govnokod.xyz/_27381
    #86: https://govnokod.ru/27405 https://govnokod.xyz/_27405
    #87: https://govnokod.ru/27429 https://govnokod.xyz/_27429
    #88: https://govnokod.ru/27432 https://govnokod.xyz/_27432
    #89: https://govnokod.ru/27435 https://govnokod.xyz/_27435
    #90: https://govnokod.ru/27439 https://govnokod.xyz/_27439
    #91: https://govnokod.ru/27449 https://govnokod.xyz/_27449
    #92: https://govnokod.ru/27460 https://govnokod.xyz/_27460
    #93: https://govnokod.ru/27463 https://govnokod.xyz/_27463
    #94: https://govnokod.ru/27466 https://govnokod.xyz/_27466
    #95: https://govnokod.ru/27473 https://govnokod.xyz/_27473
    #96: https://govnokod.ru/27478 https://govnokod.xyz/_27478
    #97: https://govnokod.ru/27484 https://govnokod.xyz/_27484
    #98: https://govnokod.ru/27495 https://govnokod.xyz/_27495
    #99: https://govnokod.ru/27504 https://govnokod.xyz/_27504
    #100: https://govnokod.ru/27508 https://govnokod.xyz/_27508
    #101: https://govnokod.ru/27511 https://govnokod.xyz/_27511
    #102: https://govnokod.ru/27518 https://govnokod.xyz/_27518

    nepeKamHblu_nemyx, 19 Июля 2021

    Комментарии (2053)
  7. Куча / Говнокод #27523

    0

    1. 1
    Тестовый Оффтоп #3

    #1: https://govnokod.ru/26373 https://govnokod.xyz/_26373
    #1: https://govnokod.ru/26611 https://govnokod.xyz/_26611
    #1: https://govnokod.ru/26824 https://govnokod.xyz/_26824
    #1: https://govnokod.ru/26850 https://govnokod.xyz/_26850
    #2: https://govnokod.ru/27102 https://govnokod.xyz/_27102

    bagrinho, 18 Июля 2021

    Комментарии (582)
  8. Куча / Говнокод #27522

    +2

    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
    ...
    
           fun([N1, _N2], Trace) ->
                   ?assert(
                      ?strict_causality( #{?snk_kind := "Adding table to a shard", shard := _Shard, live_change := true}
                                       , #{?snk_kind := "Shard schema change"}
                                       , ?of_node(N1, Trace)
                                       )),
                   ?assert(
                      ?strict_causality( #{?snk_kind := "Shard schema change", shard := _Shard}
                                       , #{?snk_kind := "Restarting shard server", shard := _Shard}
                                       , ?of_node(N1, Trace)
                                       )),
                   %% Schema change must cause restart of the replica process and bootstrap:
                   {_, Rest} = ?split_trace_at(#{?snk_kind := "Shard schema change"}, Trace),
                   ?assert(
                      ?strict_causality( #{?snk_kind := "Restarting shard server", shard := _Shard}
                                       , #{?snk_kind := state_change, to := bootstrap}
                                       , Rest
                                       ))
           end).

    Немного galaxy-brain тестов

    CHayT, 17 Июля 2021

    Комментарии (19)
  9. Куча / Говнокод #27521

    0

    1. 1
    Пиздец-оффтоп #25

    #1: https://govnokod.ru/26503 https://govnokod.xyz/_26503
    #2: https://govnokod.ru/26541 https://govnokod.xyz/_26541
    #3: https://govnokod.ru/26583 https://govnokod.xyz/_26583
    #4: https://govnokod.ru/26689 https://govnokod.xyz/_26689
    #5: https://govnokod.ru/26784 https://govnokod.xyz/_26784
    #5: https://govnokod.ru/26839 https://govnokod.xyz/_26839
    #6: https://govnokod.ru/26986 https://govnokod.xyz/_26986
    #7: https://govnokod.ru/27007 https://govnokod.xyz/_27007
    #8: https://govnokod.ru/27023 https://govnokod.xyz/_27023
    #9: https://govnokod.ru/27098 https://govnokod.xyz/_27098
    #10: https://govnokod.ru/27125 https://govnokod.xyz/_27125
    #11: https://govnokod.ru/27129 https://govnokod.xyz/_27129
    #12: https://govnokod.ru/27184 https://govnokod.xyz/_27184
    #13: https://govnokod.ru/27286 https://govnokod.xyz/_27286
    #14: https://govnokod.ru/27298 https://govnokod.xyz/_27298
    #15: https://govnokod.ru/27322 https://govnokod.xyz/_27322
    #16: https://govnokod.ru/27328 https://govnokod.xyz/_27328
    #17: https://govnokod.ru/27346 https://govnokod.xyz/_27346
    #18: https://govnokod.ru/27374 https://govnokod.xyz/_27374
    #19: https://govnokod.ru/27468 https://govnokod.xyz/_27468
    #20: https://govnokod.ru/27469 https://govnokod.xyz/_27469
    #21: https://govnokod.ru/27479 https://govnokod.xyz/_27479
    #22: https://govnokod.ru/27485 https://govnokod.xyz/_27485
    #23: https://govnokod.ru/27493 https://govnokod.xyz/_27493
    #24: https://govnokod.ru/27501 https://govnokod.xyz/_27501

    nepeKamHblu_nemyx, 16 Июля 2021

    Комментарии (2382)
  10. Куча / Говнокод #27518

    0

    1. 1
    IT Оффтоп #102

    #72: https://govnokod.ru/27120 https://govnokod.xyz/_27120
    #73: https://govnokod.ru/27136 https://govnokod.xyz/_27136
    #74: https://govnokod.ru/27160 https://govnokod.xyz/_27160
    #75: https://govnokod.ru/27166 https://govnokod.xyz/_27166
    #76: https://govnokod.ru/27168 https://govnokod.xyz/_27168
    #77: https://govnokod.ru/27186 https://govnokod.xyz/_27186
    #78: https://govnokod.ru/27219 https://govnokod.xyz/_27219
    #79: https://govnokod.ru/27254 https://govnokod.xyz/_27254
    #80: https://govnokod.ru/27270 https://govnokod.xyz/_27270
    #81: https://govnokod.ru/27280 https://govnokod.xyz/_27280
    #82: https://govnokod.ru/27284 https://govnokod.xyz/_27284
    #83: https://govnokod.ru/27296 https://govnokod.xyz/_27296
    #84: https://govnokod.ru/27336 https://govnokod.xyz/_27336
    #85: https://govnokod.ru/27381 https://govnokod.xyz/_27381
    #86: https://govnokod.ru/27405 https://govnokod.xyz/_27405
    #87: https://govnokod.ru/27429 https://govnokod.xyz/_27429
    #88: https://govnokod.ru/27432 https://govnokod.xyz/_27432
    #89: https://govnokod.ru/27435 https://govnokod.xyz/_27435
    #90: https://govnokod.ru/27439 https://govnokod.xyz/_27439
    #91: https://govnokod.ru/27449 https://govnokod.xyz/_27449
    #92: https://govnokod.ru/27460 https://govnokod.xyz/_27460
    #93: https://govnokod.ru/27463 https://govnokod.xyz/_27463
    #94: https://govnokod.ru/27466 https://govnokod.xyz/_27466
    #95: https://govnokod.ru/27473 https://govnokod.xyz/_27473
    #96: https://govnokod.ru/27478 https://govnokod.xyz/_27478
    #97: https://govnokod.ru/27484 https://govnokod.xyz/_27484
    #98: https://govnokod.ru/27495 https://govnokod.xyz/_27495
    #99: https://govnokod.ru/27504 https://govnokod.xyz/_27504
    #100: https://govnokod.ru/27508 https://govnokod.xyz/_27508
    #101: https://govnokod.ru/27511 https://govnokod.xyz/_27511

    nepeKamHblu_nemyx, 15 Июля 2021

    Комментарии (2060)