Email Gateway (Aug 22 2022 at 16:33): Email Gateway (Aug 22 2022 at 16:33):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Isabelle users,
I am struggling with the indentation rules for "if" clauses in multi-component definitions
such as inductive and function. The following example illustrates my problem:
inductive foo where
"foo some_very_long_term"
if "some_condition"
| "foo bar" if "baz"
The above is what looks like a reasonable layout to me. Unfortunately, Isabelle likes to
have it differently, namely:
inductive foo where
"foo some_very_long_term"
if "some_condition"
| "foo bar" if "baz"
Moreover, if I indent the if the way I like, auto-indent will now also indent the
subsequent | when I type it. So I end up with the following
inductive foo where
"foo some_very_long_term"
if "some_condition"
| "foo bar" if "baz"
which is not better either. IMO the "if" in an rule is subordinate to the | separating the
rules and should therefore be indented at least as far as the conclusion of the rule. Is
my understanding just wrong or is the above just an unlucky artefact of sub-optimal
indentation rules?
Andreas
Last updated: Apr 26 2024 at 01:06 UTC