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

    +2

    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, 03 Декабря 2021

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

    • ava CHayT 03.12.2021 03:15 # +2

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

    • ava CHayT 03.12.2021 12:25 # +1

      В отрефакторенном виде вроде даже нормально выглядит.
      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 03.12.2021 18:02 # 0

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

        • ava j123123 03.12.2021 20:10 # +1

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

        • ava CHayT 03.12.2021 22:35 # +2

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

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

          • ava OMuKPOH 05.12.2021 01:03 # 0

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

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