coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] What Coq function definition `Definition Term := forall T: Type, term T.` means?

From: Alex Meyer <alex153 AT outlook.lv>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] What Coq function definition `Definition Term := forall T: Type, term T.` means?
Date: Sun, 1 Jul 2018 00:24:23 +0000
Accept-language: lv-LV, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=alex153 AT outlook.lv; spf=Pass smtp.mailfrom=alex153 AT outlook.lv; spf=Pass smtp.helo=postmaster AT EUR03-AM5-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:5TspAhyk1azp/PjXCy+O+j09IxM/srCxBDY+r6Qd2+0TIJqq85mqBkHD//Il1AaPAd2Fraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HSbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHolikJKiI5/m/UhMNsg61WuwiuqwBjz4POfI2ZKORyc6XAdt0aX2pBWcNRWjRdD4O4cYQOAPcKM+FGoIj9uVQOtwa1CA62C+Pr1DBJiWL60K003uk6FgHGwRAgH9YJsHTTr9X5LqMSUf6swaTO0D7NYfRW2TLn54jJdBAsue2DXbdtccbL10YgCh7Fgk2fqYzkIzOV1vkNvHOB4+V8UuKvjnYrqxptoje12sgsiY7JhpwLxVDe+yV5xIE1JNOiREFnZt6kFZ1dvDyZOYtuWs4vTH1ktDw+x7EYo5K2fjQGxI4kyhPQc/CHfZaH7xH/WOuUJDp3mX1od66kiBu370es1PHzW8ix3VpUoCdIktrBu3UW2BDN98SLV/1w9Vq71zmVzQDc8ORELFg0laXFL54hxaY9mJUdvkrfAiP7llz6gbOReEgk4+So7P/obav8qp+bKo90lhrxMqMzmsy5HOs0KBAOX3Kc+eSgyrLs4VH5QLRNjv0wiKXZt43aJdgfpq6+BA9V0Zwv5Aq4DzejyNgYnH8HI0xZeB+fgIXlJ0vCLfTmAfulgVmgjC1nyvPJM7H5B5XCNHnDkLPvfbZn7E5czRI+wspb551KBbANPfL+V0HqudzfEx85Lwi0w+HgCNV+zI8eXXyPDreDMKzOqV+I+v4vI+6UaYAJvzb9MuEp6OLqjX8kglAQZrKp3JsSaHCgBPtqOUSZYXz2gtcAC2gGpAQ+TPa5wGGFBHRYYG/3VKYh7Bk6DpinBMHNXMrl1LeGxWKwGoBcTmFAEFGFV3nyIdaqQfAJPQuWL98ptzEVWKLpH4Yl2AH36VTSzKd7Ku3T+Wscq8Swh5BO++TPmERqpnRPBMOH3jTVFjAmriYzXzYzmZtHjwl4w1aH37J/hqUCR9tO+/dOVQR8MYCOlrUmWeC3YRrIe5KycHjjWs+vWGtjSc8tx9gJYAB5BYf6102R72+RG7YQ0oezKtk0/6bbgyejCvtHky2D/Yx8yl4sT41IKHGsgbN5+07LHYnVnk6FlqGsM6MBwCrK82TFxm2L7hhV

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?

[Coq-Club] What Coq function definition `Definition Term := forall T: Type, term T.` means?, Alex Meyer, 07/01/2018
- Re: [Coq-Club] What Coq function definition `Definition Term := forall T: Type, term T.` means?, ikdc, 07/01/2018
  - Re: [Coq-Club] What Coq function definition `Definition Term := forall T: Type, term T.` means?, Carlos Olarte, 07/01/2018
    - [Coq-Club] Atb.: What Coq function definition `Definition Term := forall T: Type, term T.` means?, Alex Meyer, 07/01/2018
      - Re: [Coq-Club] Atb.: What Coq function definition `Definition Term := forall T: Type, term T.` means?, Ralf Jung, 07/01/2018