Most predicates can be used with several instantiations modes. This directive enables the specification of each instantiation mode and the corresponding number of proofs (but not necessarily distinct solutions). The instantiation mode of each argument can include type information. You may also use this directive for documenting grammar rule non-terminals.
Template and modes¶
mode(+predicate_mode_term, +number_of_proofs) mode(+non_terminal_mode_term, +number_of_proofs)