In the same way that predicates define reusable formulas, functions define reusable expressions in Relational and Temporal Forge. Define functions with the fun keyword:

fun <fun-name>[<args>]: <result-type> {

Helper function

fun inLawA[p: Person]: one Person {

As with predicates, arguments will be evaluated via substitution. Functions may be used (with appropriate arguments) anywhere expressions can appear.

Helper function use

all p: Person | some inLawA[p]

This expands to:

all p: Person | some (p.spouse.parent1)