# Module Fact

`module Fact: `sig` .. `end``
Conjunction of hypotheses.

`type parameter = `int` `
`module ParameterMap: `Map.S``  with type key = parameter``
`type property = `fact` `
`type fact = `hypothesis Mode.ModeMap.t` `
``type hypothesis = ``
 `|` `HFalse` `|` `HConjunction of hypotheses`
`type hypotheses = `Mode.mode ParameterMap.t` `
`val conjunction : `('a -> hypothesis) -> 'a list -> hypothesis``
Conjunction of hypotheses.
`val bottom : `fact``
The least fact is defined as `constant Mode.bottom`.
`val equal : `fact -> fact -> bool``
Equality.
`val leq : `fact -> fact -> bool``
The lattice ordering.
`val join : `fact -> fact -> fact``
The lattice join (i.e., least upper bound).
`val join_many : `('a -> fact) -> 'a list -> fact``
`val meet : `fact -> fact -> fact``
The lattice meet. Beware: this operation is defined only when its left-hand argument is a fact of arity zero. (Such a fact is isomorphic to a mode. When both arguments are facts of arity zero, this operation has the same effect as `Mode.meet`.)
`val is_maximal : `fact -> bool``
Recognition of maximal facts is not performed. This function is provided for the benefit of `Fix`.
`val constant : `Mode.mode -> fact``
A mode `m` can be viewed as a fact: every mode `m'` that is equal to or above `m` is mapped to `true`, the empty conjunction, and every mode `m'` that does not satisfy this is mapped to `false`.
`val implication : `Mode.mode -> hypothesis -> fact``
`implication h m` constructs a fact of the form `h => m`. (More precisely, in this fact, the top mode is mapped to the hypothesis `trivial`; every (non-top) mode greater than or equal to `m` is mapped to the hypothesis `h`; and every other mode is mapped to the hypothesis `HFalse`.)
`val duplicable : `hypothesis -> fact``
`duplicable` is `implication ModeDuplicable`.
`val allow_exclusive : `fact -> fact``
A utility function for extending a fact with the statement ``without any hypotheses, this type is exclusive''.
`val disallow_exclusive : `fact -> fact``
A utility function for removing the possibility that ``this type is exclusive''.
`val parameter : `parameter -> fact``
A fact for a parameter `p` is a conjunction of implications of the form `m p => m`, where `m` ranges over every mode.
`val compose : `fact -> fact list -> fact``
`compose fact facts` composes a fact of arity `n` -- i.e. a fact that makes sense in the presence of `n` parameters -- with `n` facts about the actual parameters. If these facts have arity `k`, then the final fact has arity `k` as well.
`val complete : `fact -> fact``
`complete fact` completes an incomplete fact (i.e., a mode map whose domain does not contain all modes) so as to obtain a valid fact. Use with caution.
`val print : `(parameter -> PPrint.document) ->       PPrint.document -> fact -> PPrint.document``
`print param head fact` is a textual representation of the fact `fact`. The function `param` is used to map a parameter to its textual representation. `head` is a textual representation of the type that appears in the goals.
`val internal_print : `fact -> PPrint.document``
`internal_print fact` is a textual representation of the fact `fact`. Parameters are represented by their number, and there is no head. This is for internal use.