Thanks. Did you check to see if I missed any synonyms of
[Definition]/[Lemma] in my list, or shall I go check the manual and all of
the things it lists?
That's interesting. Do you happen to know how there could be an [Instance]
where I'm required to do [Proof. typeclasses eauto. Defined.] (i.e., it's
not solved automatically, but [typeclasses eauto] solves the goal)?
-Jason
On Wednesday, July 10, 2013, Pierre Courtieu wrote:
> All fixed, except that Instance cannot be indented by default because
> it is impossible to know by syntax that it starts a goal or not. The
> user should put Proof (once) when starting the proof or better: put
> curly brackets around each subgoal.
>
> P.
>
> 2013/7/10 Jason Gross <jasongro...@gmail.com <javascript:;>>:
> > Thanks!
> >
> > I have just remembered some other indentation issues I've run into, and
> > created #475-#478 (though #477 is technically highlighting, not
> > indentation).
> >
> > -Jason
> >
> >
> > On Monday, July 8, 2013, Pierre Courtieu wrote:
> >>
> >> Hi, thanks for the bug reports.
> >>
> >>
> >> 2013/7/5 Jason Gross <jasongro...@gmail.com <javascript:;>>
> >>>
> >>> Hi,
> >>>
> >>>> Except #466 are there other bugs on indentation? I don't see them.
> >>>
> >>> I have had a number of indentation issues with PG. I will go check the
> >>> bug list and file new tickets if they are not there. In short, my
> biggest
> >>> issues have been with "Arguments foo /." (adding a space after the "/"
> fixes
> >>> it)
> >>
> >>
> >> Fixed. Any combination of symbols finishing by a dot (except "..") is
> now
> >> considered a command end.
> >>
> >>> and with "{ foo : T & bar }" with a newline before/after the "&".
> >>
> >>
> >> fixed too, but I don't have generic way to deal with all operators
> >> including those defined by the user.
> >>
> >>
> >>>
> >>> I will get back to you soon with either newly reported bugs or a
> message
> >>> that these have already been reported and fixed.
> >>> Additionally, I would be curious to know if it is intentional that the
> >>> ":" in
> >>> {{
> >>> Definition foo
> >>> : T.
> >>> }}
> >>> is not indented beyond the [Definition].
> >>
> >>
> >> Good question. I tend to consider this normal because ":" is an binary
> >> operator like "+". Therefore
> >>
> >> x y
> >> + z
> >>
> >> and
> >>
> >> x y
> >> : z
> >>
> >> are correct. But I must admit it is a bit unsatisfying...
> >>
> >> P.
> >>
> >>>
> >>> -Jason
> >>>
> >>
> >>
> >
>
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
