Leanの構文を拡張する例: Maude の型を拡張する機能を取り入れる

(個人的なメモですがここに書きたいと思ったのでここに置かせてもらいます 🙇 )

「これが出来たらLeanの拡張性の高さを伝える良い例になる」と感じたので実装してみたい機能

元ネタは https://github.com/Seasawher/Maude.lean/blob/5e119ec0cd3706d0e6dfabffb31e5cdec7e9872a/Maude/Nat.lean#L197

Maudeでは以下のように、既存の型Natに新しいコンストラクタinf(∞を意図する値)を追加し、Nat上の関数 succ + * を少ない記述で「拡張したNat」に対応させることができる

fmod NAT-EXT is
  pr(NAT-MULT) .
  op inf : -> Nat .
  var N N1 N2 : Nat .
  eq succ(inf) = inf .
  eq inf + N = inf .
  eq N + inf = inf .
  eq inf * 0 = 0 .
  eq 0 * inf = 0 .
  eq inf * succ(N) = inf .
  eq succ(N) * inf = inf .
endfm

この機能をLeanで実装したい。
構文だけは定義したが、コマンドとしてちゃんと動くように実装するにはまだ知識が足りないので、メタプロ力が上がった時にまた挑戦したい。

ちなみに、以下で定義した構文ではAdd MulやOfNatのような型クラスを継承することは考えていない
(一旦スコープ外)

import Lean

open Lean Parser Elab Command

declare_syntax_cat funExt
syntax ident declValEqns : funExt

elab "extend " term " with " ident ("(" str ")")? " => " ident "inherits" funExt* : command => do
  logInfo "未実装"

extend Nat with inf ("∞") => ENat
  inherits
    succ
      | inf => inf
    add
      | inf, _ | _, inf => inf
    mul
      | 0, _ | _, 0 => 0
      | inf, n + 1 | n + 1, inf => inf

#check_failure ENat
#check_failure ENat.succ
#check_failure ENat.add
#check_failure ENat.mul

-- ↓こういう結果になってほしい

def ENat := Option Nat
@[match_pattern] abbrev ENat.inf : ENat := none
notation "∞" => ENat.inf

def ENat.succ : ENat → ENat
  | some n => some (Nat.succ n)
  | inf => inf

def ENat.add : ENat → ENat → ENat
  | some m, some n => some (Nat.add m n)
  | inf, _ | _, inf => inf

def ENat.mul : ENat → ENat → ENat
  | some m, some n => some (Nat.mul m n)
  | some 0, _ | _, some 0 => some 0
  | inf, some (n + 1) | some (n + 1), inf => inf
  -- ↓ のパターンがなくて怒られているが、このエラーがコマンドの`mul`のところに出てほしい
  -- | inf, inf => inf

Start with the issue's declare_syntax_cat funExt and elab "extend" command, then compare the referenced Maude/Nat.lean example. Done means the command implements the shown ENat definitions and reports missing patterns such as inf, inf at the relevant declaration.