Rework nouns (MObj/MathCN) and introduce declarations
Current Situation
We have the categories MObj
, which represents common nouns like
- positive integer
n
- abelian group
- ...
We also have the category MathCN
, which represents formulae that introduce an identifier, like n
or $0 < k < 2$.
A MathCN
can be appended to an MObj
in an apposition ("an integer n
").
TODO
Develop a way to deal with nouns properly in a way that can handle declarations as well. Then, write a new issue with a description for the actual implementation.
Observations
There are at least two different ways how a formula can correspond to a noun (currently, MathCN
corresponds only to the first one):
-
With identifier: "
n
", "a \in S
", ... -
Without identifier: "there is a bijection from
[0, 1]
to(0, 1)
", ...
Example sentences
- Let
n
be a positive integer - For every positive integer
n
- For every
n \in N
- For every divisor
d
of a natural numbern
- A positive integer
n
is - Let
S = {s_1, ..., s_n}
be a finite set of integers