如何打印decreasing_by中递归函数终止性证明的显式形式？

Lean会自动为递归函数的终止性证明生成辅助定理，你可以通过以下几种方式找到并打印它：

• 直接打印自动生成的证明项：Lean对单终止度量的递归函数，通常会将终止性证明命名为函数名._proof_1。针对你的代码，执行：

  #print LAMt.occurs_free_in._proof_1
  

  若存在多个终止条件，可尝试._proof_2等后缀。

• 列出所有相关辅助项：如果不确定具体名称，用#print prefix查看所有以目标函数开头的项：

  #print prefix LAMt.occurs_free_in
  

  输出结果中会包含终止性证明的完整名称。

• 查看完整显式结构：开启全打印选项后再执行#print，能展开所有隐式参数和内部构造：

  set_option pp.all true
  #print LAMt.occurs_free_in._proof_1
  

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