Module Signature.Declaration

type t =
  1. | Typ of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Identifier.t;
    3. kind : Synext__.Synext_definition.LF.Kind.t;
    }
    (*

    LF type-level constant declaration.

    *)
  2. | Const of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Identifier.t;
    3. typ : Synext__.Synext_definition.LF.Typ.t;
    }
    (*

    LF term-level constant declaration.

    *)
  3. | CompTyp of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Identifier.t;
    3. kind : Synext__.Synext_definition.Comp.Kind.t;
    4. datatype_flavour : [ `Inductive | `Stratified ];
    }
    (*

    Computation-level data type constant declaration.

    *)
  4. | CompCotyp of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Identifier.t;
    3. kind : Synext__.Synext_definition.Comp.Kind.t;
    }
    (*

    Computation-level codata type constant declaration.

    *)
  5. | CompConst of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Identifier.t;
    3. typ : Synext__.Synext_definition.Comp.Typ.t;
    }
    (*

    Computation-level type constructor declaration.

    *)
  6. | CompDest of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Identifier.t;
    3. observation_type : Synext__.Synext_definition.Comp.Typ.t;
    4. return_type : Synext__.Synext_definition.Comp.Typ.t;
    }
    (*

    Computation-level type destructor declaration.

    *)
  7. | Schema of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Identifier.t;
    3. schema : Synext__.Synext_definition.Meta.Schema.t;
    }
    (*

    Declaration of a specification for a set of contexts.

    *)
  8. | Recursive_declarations of {
    1. location : Syncom.Location.t;
    2. declarations : t Support.List1.t;
    }
    (*

    Recursive declaration(s).

    *)
  9. | Theorem of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Identifier.t;
    3. typ : Synext__.Synext_definition.Comp.Typ.t;
    4. order : Totality.Declaration.t Support.Option.t;
    5. body : Synext__.Synext_definition.Comp.Expression.t;
    }
    (*

    Beluga theorem declaration.

    *)
  10. | Proof of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Identifier.t;
    3. typ : Synext__.Synext_definition.Comp.Typ.t;
    4. order : Totality.Declaration.t Support.Option.t;
    5. body : Synext__.Synext_definition.Harpoon.Proof.t;
    }
    (*

    Harpoon proof declaration.

    *)
  11. | CompTypAbbrev of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Identifier.t;
    3. kind : Synext__.Synext_definition.Comp.Kind.t;
    4. typ : Synext__.Synext_definition.Comp.Typ.t;
    }
    (*

    Declaration for a computation-level type function. The parameters introduced by Pi-kinds in kind are parameters to the type typ.

    *)
  12. | Val of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Identifier.t;
    3. typ : Synext__.Synext_definition.Comp.Typ.t Support.Option.t;
    4. expression : Synext__.Synext_definition.Comp.Expression.t;
    }
    (*

    Computation-level value declaration.

    *)
  13. | Module of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Identifier.t;
    3. entries : Entry.t Support.List.t;
    }
    (*

    Namespace declaration for other declarations.

    *)

Parsed signature element