Custom Query (361 matches)

The following two blocks of code have been indented by highlighting the lines and pressing TAB:

Incorrect indentation:

Section foo.
  Arguments id /.
            Definition foo := Type.
  Definition bar := Type.
End foo.

Correct indentation:

Section foo.
  Arguments id / .
  Definition foo := Type.
  Definition bar := Type.
End foo.

Here's some code formatted by TAB in emacs PG:

Definition A
: { T : ReallySuperDuperExtremelyLongName bar baz qux &
                                          foo T }.
  Definition B
  : { T : (ReallySuperDuperExtremelyLongName bar baz qux) &
                                                          foo T }

      Definition C
  : { T : ReallySuperDuperExtremelyLongName bar baz qux
                                            & foo T }.
    Definition D
    : { T : (ReallySuperDuperExtremelyLongName bar baz qux)
              & foo T }

The indentation of Definition is clearly broken. Additionally, I think all of them should be formatted roughly like Definition D, where the & or the foo is lined up close to the start of the line, rather than as an argument of ReallySuperDuperExtremelyLongName. I'd be even happier if sigT notation were formatted like sig notation, that is, if & acted like | here. (This change doessn't fix the screwy levels of Definition, though.)

Here is some code indented by TAB:

Goal True.                                                                                                                                  
Proof.
  match goal with
    | _ => exists 1
                | _ => idtac
                  end.