package rocq-runtime

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

Module Extern.RecordsSource

Sourcetype t
Sourceval make_raw : t -> t
Sourceval current : unit -> t
Sourceval current_ignore_raw : unit -> t
Sourceval use_record_syntax : t -> Names.inductive -> bool

Tells whether record syntax should be used for some record. If the inductive is not a record, the result is meaningless.