Соглашения о стиле кодирования в Изабель / Изаре
TL; DR: Существуют ли соглашения по кодированию для языка Изара? Нужно ли соблюдать стратегию сворачивания jEdit?
Моя команда работает над формализацией математики, поэтому одной из наших основных целей является получение удобочитаемых доказательств. Рассматривая это, мы попытались закодировать доказательства таким образом, чтобы выделить промежуточные факты (и ярлыки, если таковые имеются):
from fact1 have
1: "Foo"
using Thm1 Thm2 by auto
then have
2: "Bar = FooBar"
by simp
also from 1 have
" ... = BarFoo"
by blast
и т. д. Помимо того, что иногда это приводит к распространению "коротких линий" (кстати, я не знаю, действительно ли это проблема), это как-то несовместимо со стратегией сворачивания jEdit; после сворачивания предыдущий блок кода будет выглядеть так:
from fact1 have
then have
also from 1 have
полностью скрывая аргумент. Следующий формат, возможно, лучше:
from fact1
have 1: "Foo"
using Thm1 Thm2 by auto
then
have 2: "Bar = FooBar"
by simp
also from 1
have " ... = BarFoo"
by blast
И, после складывания,
from fact1
have 1: "Foo"
then
have 2: "Bar = FooBar"
also from 1
have " ... = BarFoo"
который делает поток аргумента явным.
В любом случае, прежде чем я придумаю 5 новых соглашений о форматировании, я бы определенно хотел узнать, существует ли какой-то де-факто стандарт, или, по крайней мере, если кто-то подумал об этом.