kinds of FMPs (definitional, computational) specify it clearly.

[kohlhase]

Abstract CD spec in OM2 says that FMPs can have types, but not more. This should be specified (see OpenMath/OM3#125). And there are two specific kinds that are proposed.

• definitional (see FMP type=defining OM3#5)
• alias (see FMP type=alias OM3#32)
• computational (see see Introduce computational FMPs OM3#129)

[car222222]

Some maybe ‘useful facts’ = ‘theorems’ rather than ‘definitions’. And typical maths definitions can involve a lot of ‘assumptions’ = ‘theorems’.