Remove the indentation restriction on pref environment

[Lev135]

Проблема в следующем:

@Theorem
  some theorem

> a + b = c

Если перед > a + b = c необходимо делать отступ (как сейчас), то формула попадает внутрь окружения @Theorem. На данный момент такое можно решить только хаком:

@Theorem
  Условие теоремы

%
  > a + b = c

но это выглядит не очень. Также из-за этого есть ограничение на отступ ровно в два пробела в окружениях -- иначе не получается распарсить

@Theorem
    > x = y
  Условие теоремы

Если же убрать ограничение на отступ, то его можно будет делать по своему усмотрению и всё будет работать

[Lev135]

Таким образом, предполагаемые правила такие:

1. Если строка начинается с @<some-name>, то это окружение <some-name>. Тогда всё что далее имеет больший отступ находится внутри него
2. Если строка начинается не с (буквы | цифры | @ | | ) то это это префикс (до первого пробела) и далее всё как с обычным окружением
3. Если не 1 и не 2 -- это просто Paragraph

P. S. символ | зарезервирован для префиксов с параметрами:

| Pif > a^2 + b^2 = c^2

создаёт нумерованную формулу, а по Pif можно будет на неё ссылаться (при соответствующем определении >)

[Lev135]

Чтобы быть совсем последовательным, логично было б запретить вообще отступы перед префиксным окружением, как и перед абзацем, но тогда текст становится сильно менее читаемым:

Докажем выводимость аксиом Лёба. 
- `J |- <*>p -> <*>(p /\ ~<*>p)`\\
  Применяя аксиому Лёба для `<0>`:
  > J |- <0>(<1>T /\ p) -> <0>(<1>T /\ p /\ ~<0>(<1>T /\ p))
  с точностью до обозначения `<*>\cdot = <0>(<1>T /\ \cdot)` это и есть требуемое
- `J |- <*>^2 p -> <*>^2(p /\ ~<*>^2 p)`\\
  Из предыдущего пункта, пользуясь нормальностью `<*>`:
  > J |- <*>^2 p -> <*>^2(p /\ ~<*>p)
  Осталось воспользоваться тем, что `GL(<*>) |- <*>^2 p -> <*>p`
- `J |- <0><1>p -> <0><1>(p /\ ~<0><1>p)`\\
  По аксиоме Лёба
  > J |- <0><1>p &-> <0>(<1>p /\ ~<0><1>p)
    <1>p &-> <1>(p /\ ~<1>p)
  Пользуясь тем, что `J |- ~<0><1>p -> [1](~<0><1>p)` по нормальности получаем требуемое
- `J |- <1>T /\ <*>p -> <1>T /\ <*>(p /\ (~<1>T \/ ~<*>p))`\\
  Следует из аксиомы Лёба для `<*>`

vs

Докажем выводимость аксиом Лёба. 
  - `J |- <*>p -> <*>(p /\ ~<*>p)`\\
    Применяя аксиому Лёба для `<0>`:
      > J |- <0>(<1>T /\ p) -> <0>(<1>T /\ p /\ ~<0>(<1>T /\ p))
    с точностью до обозначения `<*>\cdot = <0>(<1>T /\ \cdot)` это и есть требуемое
  - `J |- <*>^2 p -> <*>^2(p /\ ~<*>^2 p)`\\
    Из предыдущего пункта, пользуясь нормальностью `<*>`:
      > J |- <*>^2 p -> <*>^2(p /\ ~<*>p)
    Осталось воспользоваться тем, что `GL(<*>) |- <*>^2 p -> <*>p`
  - `J |- <0><1>p -> <0><1>(p /\ ~<0><1>p)`\\
    По аксиоме Лёба
      > J |- <0><1>p &-> <0>(<1>p /\ ~<0><1>p)
        <1>p &-> <1>(p /\ ~<1>p)
    Пользуясь тем, что `J |- ~<0><1>p -> [1](~<0><1>p)` по нормальности получаем требуемое
  - `J |- <1>T /\ <*>p -> <1>T /\ <*>(p /\ (~<1>T \/ ~<*>p))`\\
    Следует из аксиомы Лёба для `<*>`

[Lev135]

Есть решение такое: ещё больше ограничить размеры отступа, внутренность окружения должна отступать на двойной отступ, а префиксное окружение -- на одинарный. Тогда первая проблема решается так:

@Theorem
   some theorem

 > a + b = c
Next paragraph