Module `Signature.Totality`

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

For instance, the named totality declaration

  / total [x y z] (f x y z w) /

specifies that the function named f is checked for totality using the lexical ordering [x y z] of its arguments.

module Declaration : sig ... end

module Order : sig ... end

Totality argument orderings for totality-checking.