Re: [isabelle] Isabelle style guide
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Isabelle style guide
- From: Lars Noschinski <noschinl at in.tum.de>
- Date: Mon, 01 Jun 2015 15:23:13 +0200
- In-reply-to: <alpine.LNX.email@example.com>
- References: <9ACE55FB-A37E-4A63-BF9C-5F484ECBF8E2@nicta.com.au> <alpine.LNX.firstname.lastname@example.org> <E0896D6C-CD27-4F5A-ADF3-6E573E18B3CF@nicta.com.au> <alpine.LNX.email@example.com>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.7.0
On 30.05.2015 23:09, Makarius wrote:
> definition foo :: T where
> "foo = ..."
This is the form I use most. It only uses two lines and keeps as much
space as possible for the actual definition. I don't mind seeing the
unnecessary "where" in the sidekick -- it is at the end of the line,
after all. Also, seeing the name suffices for my purposes, so even the
type is unnecessary (for me).
I mostly use the sidekick to see the section structure. I would like to
see more information about my lemmas there (instead of just the name),
but I almost always state my lemmas in structured form, so I have a line
break after name.
This archive was generated by a fusion of
Pipermail (Mailman edition) and