Module Signature.Declaration

type t =
  1. | Raw_lf_typ_or_term_constant of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Identifier.t;
    3. typ_or_const : Synprs__.Synprs_definition.LF.Object.t;
    }
  2. | Raw_lf_typ_constant of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Identifier.t;
    3. kind : Synprs__.Synprs_definition.LF.Object.t;
    }
  3. | Raw_lf_term_constant of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Identifier.t;
    3. typ : Synprs__.Synprs_definition.LF.Object.t;
    }
  4. | Raw_inductive_comp_typ_constant of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Identifier.t;
    3. kind : Synprs__.Synprs_definition.Comp.Sort_object.t;
    }
  5. | Raw_stratified_comp_typ_constant of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Identifier.t;
    3. kind : Synprs__.Synprs_definition.Comp.Sort_object.t;
    }
  6. | Raw_comp_cotyp_constant of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Identifier.t;
    3. kind : Synprs__.Synprs_definition.Comp.Sort_object.t;
    }
  7. | Raw_comp_expression_constructor of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Identifier.t;
    3. typ : Synprs__.Synprs_definition.Comp.Sort_object.t;
    }
  8. | Raw_comp_expression_destructor of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Identifier.t;
    3. observation_type : Synprs__.Synprs_definition.Comp.Sort_object.t;
    4. return_type : Synprs__.Synprs_definition.Comp.Sort_object.t;
    }
  9. | Raw_comp_typ_abbreviation of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Identifier.t;
    3. kind : Synprs__.Synprs_definition.Comp.Sort_object.t;
    4. typ : Synprs__.Synprs_definition.Comp.Sort_object.t;
    }
  10. | Raw_schema of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Identifier.t;
    3. schema : Synprs__.Synprs_definition.Meta.Schema_object.t;
    }
  11. | Raw_theorem of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Identifier.t;
    3. typ : Synprs__.Synprs_definition.Comp.Sort_object.t;
    4. order : Totality.Declaration.t Support.Option.t;
    5. body : Synprs__.Synprs_definition.Comp.Expression_object.t;
    }
  12. | Raw_proof of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Identifier.t;
    3. typ : Synprs__.Synprs_definition.Comp.Sort_object.t;
    4. order : Totality.Declaration.t Support.Option.t;
    5. body : Synprs__.Synprs_definition.Harpoon.Proof.t;
    }
  13. | Raw_recursive_declarations of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. declarations : t Support.List1.t;
    }
  14. | Raw_val of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Identifier.t;
    3. typ : Synprs__.Synprs_definition.Comp.Sort_object.t Support.Option.t;
    4. expression : Synprs__.Synprs_definition.Comp.Expression_object.t;
    }
  15. | Raw_module of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Identifier.t;
    3. entries : Entry.t Support.List.t;
    }