Module Synext.Signature

module Pragma : sig ... end

Signature pragmas for setting compilation parameters

module Global_pragma : sig ... end

Global signature pragmas for setting compilation parameters

module Totality : sig ... end

Totality declarations and orderings for configuring the totality checker for theorems and proofs.

module Declaration : sig ... end
module Entry : sig ... end
type signature_file = {
  1. location : Syncom.Location.t;
  2. global_pragmas : Global_pragma.t Support.List.t;
  3. entries : Entry.t Support.List.t;
}