类型和编程语言：Abb代表什么？

问题描述

在TAPL的全简单类型示例中。 TmAbb代表什么？

| TmVar(fi,n,_) ->
  (match getbinding fi ctx n with
      TmAbbBind(t,_) -> t 
    | _ -> raise noruleApplies)

解决方法

翻阅这本书，似乎“ Tm”代表“ term”，但我在任何地方都看不到“ Abb”。

但是，我下载了代码（fullsimple.tar.gz），正如您所说的，有一个构造函数“ TmAbbBind”。这是一种约束，而不是一种术语。特别是，它似乎是一个术语的绑定以及可以通过名称查找的相关可选类型。

因此，我猜它代表“术语缩写绑定”。即，术语缩写必须绑定。