Module Totality.Declaration

type t =
  1. | Trust of {
    1. location : Syncom.Location.t;
    }
    (*

    Trust _ is the totality declaration trust which indicates that the totality of the annotated function is not checked.

    *)
  2. | Numeric of {
    1. location : Syncom.Location.t;
    2. order : Support.Int.t Order.t Support.Option.t;
    }
    (*
    • Numeric { order = Option.None; _ } is the totality declaration total which indicates that the annotated function should be checked for totality without totality argument.
    • Numeric { order = Option.Some order; _ } is the totality declaration total order which indicates that the annotated function should be checked for totality with order.
    *)
  3. | Named of {
    1. location : Syncom.Location.t;
    2. order : Syncom.Identifier.t Order.t Support.Option.t;
    3. program : Syncom.Identifier.t;
    4. argument_labels : Syncom.Identifier.t Support.Option.t Support.List.t;
    }
    (*
    • Named { order = Option.None; program = "f"; argument_labels = ["x1"; "x2"; ...; "xn"]; _ } is the totality declaration total (f x1 x2 ... xn) which indicates that the annotated function should be checked for totality without totality argument.
    • Named { order = Option.Some order; program = "f"; argument_labels = ["x1"; "x2"; ...; "xn"]; _ } is the totality declaration total x (f x1 x2 ... xn) which indicates that the annotated function should be checked for totality with order.
    *)