I'm trying to explore the possibility of using Template Coq functions such as tmMkDefinition to construct Records and/or Classes. I can construct an inductive with a single constructor and all the field projections. Is there a way using MetaCoq to better mimic what Coq does when a Record is defined (e.g., allowing the projections to be using the field syntax)? Or is this the best that can be done?

I don't fully understand the question I think. Are you saying the records defined using MetaCoq and records defined manually in Coq behave differently?

I can use tmMkInductive' to construct an inductive with a single constructor which has the same "internal structure" as a Coq-defined record, but if I run Print, it prints as an Inductive and not as a Record. Similarly, the field projections aren't automatically defined; I can define them myself using MetaCoq, but the record.(field) notation won't work.

Potentially relevant bit in the Coq kernel: https://github.com/coq/coq/blob/315590487491821a8ff285f5e47415dca7827d35/kernel/declarations.mli#L142

More directly relevant: https://github.com/MetaCoq/metacoq/blob/943cc72bd12ab41d1f67af96f5744c32e40338bf/erasure/theories/EAst.v#L122; this is used in https://github.com/coq/coq/blob/315590487491821a8ff285f5e47415dca7827d35/kernel/indtypes.ml#L580

EAst shouldn't be relevant, the parts related to the template monad will be in `TemplateCoq.Ast`

IIUC, you'd need `mind_entry_record := Some None`

to get a (non-primitive) record, and `Some (Some ...)`

for primitive records?

(EAst and Ast are similar, but EAst is after type and proof erasure)

Thanks, https://github.com/MetaCoq/metacoq/blob/943cc72bd12ab41d1f67af96f5744c32e40338bf/template-coq/theories/Ast.v#L736 then?

Yes, that looks right

Thank you!

Last updated: Jul 23 2024 at 20:01 UTC