Isabelle中如何为函数定义下标形式的可读性缩写？

要把myf n a替换成fₙ a这种可读性更强的下标形式，你需要修正两个问题：Isabelle不支持用HTML的<sub>标签定义语法，且定义体的函数名必须和声明的myf保持一致。正确写法如下：

• 定义带语法缩写的函数
  使用Isabelle内置的下标命令\<^sub>来指定缩写格式，定义体仍用原函数名myf：

  definition myf :: "nat => nat => nat" ("f\<^sub>_ _" [90]) where
    "myf n a = n * a"
  

• 使用缩写
  之后就能用f\<^sub>n a替代myf n a，Isabelle会自动将\<^sub>n渲染为下标样式的fₙ a。

• 备选方案：直接用Unicode下标
  如果你习惯输入Unicode下标字符（如ₙ），也可以这样定义：

  definition myf :: "nat => nat => nat" ("fₙ _" [90]) where
    "myf n a = n * a"
  

  不过这种方式的占位符灵活性稍差，更推荐用\<^sub>_的形式适配任意下标参数。

你之前报错的原因是：定义体里误用了f<sub>n</sub> a作为函数名，但Isabelle要求定义的头部必须是声明的myf——带下标的形式只是语法层面的缩写，并非函数的实际标识符。

内容的提问来源于stack exchange，提问作者Alicia M.