Stream: Ltac2

Topic: Definition of list

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Feb 04 2022 at 13:04):

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

view this post on Zulip Gaëtan Gilbert (Feb 04 2022 at 13:06):

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

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 13:32):

I see.

Last updated: Apr 20 2024 at 01:41 UTC