It should be possible to get the projections of records from Ltac2 - Githubissues

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

https://coq.inria.fr/

GNU Lesser General Public License v2.1

4.84k stars 647 forks source link

It should be possible to get the projections of records from Ltac2 #17874

Open JasonGross opened 1 year ago

JasonGross commented 1 year ago

I'd like to port https://github.com/tchajed/coq-record-update-plugin/blob/master/src/eta_expansion.ml to Ltac2

I guess the primary requirement is having accessible from Ltac2 https://github.com/coq/coq/blob/632d118bea99b0abd76b3cc54c54873e7110ed63/pretyping/structures.mli#L46-L52 and maybe also for primitive projections having https://github.com/coq/coq/blob/632d118bea99b0abd76b3cc54c54873e7110ed63/pretyping/structures.mli#L159-L161

Some design questions (is there a doc of design principles for the Ltac2 interface @ppedrot @MSoegtropIMC @coq/ltac2-maintainers ?):

Should find_projections raise Not_found or should it return an option type?
Should this all live in Ltac2.Structures.*, or Ltac2.Structures.Structure.*, or just Ltac2.Ind.*?
Are the names fine, or do we want to adjust them?

tchajed commented 1 year ago

This seems like a great idea! The Ltac2 version would be immediately shippable whereas people are unlikely to add a plugin dependency.