问题描述
在TAPL的全简单类型示例中。 TmAbb代表什么?
| TmVar(fi,n,_) ->
(match getbinding fi ctx n with
TmAbbBind(t,_) -> t
| _ -> raise NoRuleApplies)
解决方法
翻阅这本书,似乎“ Tm”代表“ term”,但我在任何地方都看不到“ Abb”。
但是,我下载了代码(fullsimple.tar.gz),正如您所说的,有一个构造函数“ TmAbbBind”。这是一种约束,而不是一种术语。特别是,它似乎是一个术语的绑定以及可以通过名称查找的相关可选类型。
因此,我猜它代表“术语缩写绑定”。即,术语缩写必须绑定。