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 var repeatedly within the definition? I think term receives an element of type type. Does it mean term also need to an argument of type var?
See https://coq.inria.fr/refman/language/core/sections.html ; Coq Sections are a way to introduce variables in the context of a family of definitions without mentioning them repeatedly in signatures. A bit as if you wrote “all the following theorems are quantified on n, which we omit for brevity”.
For example here’s a section from List.v in Coq’s library:
Section Map.
Variables (A : Type) (B : Type).
Variable f : A -> B.
Fixpoint map (l:list A) : list B :=
match l with
| [] => []
| a :: t => (f a) :: (map t)
end.
Lemma map_cons (x:A)(l:list A) : map (x::l) = (f x) :: (map l).
Proof.
reflexivity.
Qed.
Notice how the Fixpoint and the Lemma don’t repeat the variables “A”, “B”, and “f”.
Yet at the end of the section the signature of map is map : forall [A B : Type], (A -> B) -> list A -> list B, so these variables get “generalized” eventually.
