The Coq mailing list

[ikdc <ikdc AT mit.edu>]

Looks like a PHOAS construction; see http://adam.chlipala.net/papers/PhoasICFP08/ for details.

(Reference [4] in the paper you linked.)

On Jun 30, 2018 20:24, Alex Meyer <alex153 AT outlook.lv> wrote:

I am reading about mechanization of linear logic in Coq

http://www.cs.cmu.edu/~iliano/projects/metaCLF2/inc/dl/papers/lsfa17.pdf and

https://github.com/brunofx86/LL and I have trouble to understand the the function definition Term(and other function definitions involving forall) from

https://github.com/brunofx86/LL/blob/master/FOLL/LL/SyntaxLL.v:

Definition Term := forall T:Type,  term T. (* type for terms *)
Definition AProp := forall T:Type, aprop T. (* type for atomic propositions *)

Why we need forall construction in function definition, what additional meaning it gives? Is is creating some kind of set - i.e. - that function returns set of results - one result for each type.

I asked this question on stackoverflow:

https://stackoverflow.com/questions/51017013/what-coq-function-definition-definition-term-forall-t-type-term-t-means

and received one answer there but I would like to get more elaborate answer, I still does not understand this this construction. Maybe there is some good and exact reference in literature?