package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Record.Record_declSource

A record is an inductive mie with extra metadata

Sourcetype t = {
  1. entry : RecordEntry.t;
  2. records : Data.t list;
  3. projections_kind : Decls.definition_object_kind;
  4. indlocs : DeclareInd.indlocs;
}