Terms occur on the object level; specifically as components of declarations, most notably as types and definitions of constants. They represent syntax trees with binding, e.g. first-order terms and formulas, types, lambda expressions etc.
Terms are defined recursively:
The precise abstract syntax is explained in more detail here.
In the MMT language, terms are given by using symbol/variable names and the notations of the symbols in the current context (previous declarations in the containing module). Binders extend the current context for their arguments by the variables they bind.
a + (b ⋅ c) would be an application (OMA) of a symbol
+ (OMS) to a symbol
a (OMS) and (an application (OMA) of a symbol
⋅ (OMS) to a symbol
b (OMS) and a symbol
c (OMS)). We can write this as:
+,⋅,a,b,c have to be in context, of course.
λx:t. x+a would be a binding application (OMBIND) binding a variable
x of type
t to (an application of …). We can write this as:
λ extends the inner context of the argument by the variable
x, guaranteeing that
x+a is a well-formed term.