CODEWITHSUNDEEP
ocamlprogramming-languageslambda-calculustype-theory
databasechaser
databasechaser

Reputation: 341

Types and Programming Languages: What does Abb stand for?

In TAPL's example of fullsimple type. What does TmAbb stand for?

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

Upvotes: 0

Views: 105

Answers (1)

Jeffrey Scofield
Jeffrey Scofield

Reputation: 66793

Looking through the book, it appears that "Tm" stands for "term" but I don't see "Abb" anywhere.

However, I downloaded the code (fullsimple.tar.gz) and there is a constructor "TmAbbBind" just as you say. It's a kind of binding, not a kind of term. In particular it seems to be a binding for a term and an associated optional type that can be looked up by name.

So "term abbreviation binding" is what it stands for I guess. I.e., it's the thing that a term abbreviation is bound to.

Upvotes: 1

Related Questions