Stream: MetaCoq

Topic: Descriptions of fields of record types in template-coq

Julin S (Jan 03 2022 at 04:31):

Is there a place where we can read about the purpose and a description of the fields of the various record types available in template-coq?

For example, the definition of mutual_inductive_body

Record mutual_inductive_body : Type := Build_mutual_inductive_body
  { ind_finite : recursivity_kind;
    ind_npars : nat;
    ind_params : context;
    ind_bodies : list one_inductive_body;
    ind_universes : universes_decl;
    ind_variance : option (list Variance.t) }

but couldn' t understand what the data in each of these fields stand for.

The docs (which has some info but not too much) advise to look in a file name declarations.ml but couldn't find such a file upon searching the metacoq repo.

Julin S (Jan 03 2022 at 04:32):

Or could it be that coq's documentation itself cover this?

Julin S (Jan 03 2022 at 04:33):

Oh.. I guess this is the declarations.ml file: https://github.com/coq/coq/blob/master/kernel/declarations.ml

And the comments describe what they do.

Sorry should've looked a bit further before.

Théo Winterhalter (Jan 03 2022 at 07:23):

Perhaps the pointer to declarations.ml should more explicitly state that it's referring to the source of coq?

Last updated: Oct 01 2023 at 18:01 UTC