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 number $n$
- A positive integer $n$ is
- Let $S = {s_1, ..., s_n}$ be a finite set of integers