Lean 4 4.0.0-nightly版本#check Nat.add输出异常如何解读？

这不是乱码，而是该夜间版本的临时格式改动，具体说明如下：

• a✝和a✝¹是Lean内部用于标识匿名占位参数的符号，其中✝标记临时/无名变量，¹是区分重复匿名参数的下标。
• 当时的版本尝试让#check输出更贴近函数调用的直观形式，把原本标准的函数类型表示Nat.add : Nat → Nat → Nat，改成了模拟函数调用的写法：Nat.add (参数1 : Nat) (参数2 : Nat) : Nat，只是用匿名标记替代了显式参数名。
• 该改动因可读性不佳被社区反馈，所以在Lean 4.8版本中被撤销，输出恢复为传统的箭头类型格式。

内容的提问来源于stack exchange，提问作者pygri