Hi, I am reading the paper “Parametric Higher-Order Abstract Syntax for Mechanized Semantics” and have a question.
The paper says “Figure 5 shows Coq code for this syntax formalization scheme.
We use Coq’s “sections” facility to parameterize the term type
with a type family var without needing to mention var repeatedly
within the definition.” I cannot understand the sentence. Why we do not need to mention
varrepeatedly within the definition? I think
termreceives an element of type
type. Does it mean
termalso need to an argument of type