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

0

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
Ltac2 make_match fields :=
  destruct x;
  iter (fun a => focus 1 1 (fun () =>
                           let a := a ()
                           in refine (fun () => '((w_rep $a) _)))
         ) fields.

Итерация по конструкторам индуктивного типа данных.

Запостил: CHayT CHayT, (Updated )

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

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

    В Coq 8.12 не было волшебного модуля Ltac2.Ind, который даёт нормальный доступ к индуктивным типам данных, в качестве POC высралась такая метушня для создания паттерн-матчинга
    Ответить

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

    В отрефакторенном виде вроде даже нормально выглядит.
    Ltac2 derive_ret_t fields :=
  refine (fun () => '(fun a => _));
  Std.case false (hyp @a, NoBindings);
  iter (fun rep_t =>
          focus 1 1 (fun () => refine (fun () => rep_t ()))
       ) fields.

    Вообще, Ltac2 начинает мне нравиться, правда чтобы понять, как на нём писать, пришлось прочитать его код и его тесты, настолько ужасна документация.
    Ответить

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

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

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

        Ма-те-ма-тики к тому моменту изобретут еще более заумную ма-те-ма-тическую питушню, которую смузихлебы не осилят, и будут с ней пердолиться.
        Ответить

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

        > на багованном JS-подобном скриптоговне

        На оригинальном Ltac то есть?
        Ответить

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

          Могу предложить тебе отличную программу на языке аминокислот.
          Для установки тебе достаточно лишь регулярно облизывать кончики пальцев.
          Ответить

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

Где здесь C++, guest?!

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

    ↑
    8
    ↓