Stream: Ltac2

Topic: Definition of list

Guillaume Melquiond (Feb 04 2022 at 12:53):

I am trying to find the definition of the list type (and its constructors). Even builtin types, e.g., int, are defined in Ltac2/Init.v. But I cannot find any trace of list.

Gaëtan Gilbert (Feb 04 2022 at 13:04):

probably https://github.com/coq/coq/blob/ec603750e780dc3017d6aeed6b1657995680b102/plugins/ltac2/tac2entries.ml#L1046-L1054

Gaëtan Gilbert (Feb 04 2022 at 13:06):

possibly because the constructor names aren't valid in ltac2 syntax

Guillaume Melquiond (Feb 04 2022 at 13:32):

I see.

Last updated: May 31 2023 at 10:01 UTC