Re: [isabelle] Several questions about coding style/best practices
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Several questions about coding style/best practices
- From: Wolfgang Jeltsch <wolfgang-it at jeltsch.info>
- Date: Mon, 08 Jul 2019 16:34:37 +0300
- In-reply-to: <CALaF1UJQ_Dfg26rFY=CRFhh4jHf9zM3G-ChaZ3cwtnN3p3iT-Q@mail.gmail.com>
- References: <CALaF1UJQ_Dfg26rFY=CRFhh4jHf9zM3G-ChaZ3cwtnN3p3iT-Q@mail.gmail.com>
Following are some of my personal style decisions.
> 1. Should `⟦ S ⊆ 𝔘; T ⊆ 𝔘; τ S; τ T ⟧ ⟹ τ (S ∩ T)` be preferred
> over `S ⊆ 𝔘 ⟹ T ⊆ 𝔘 ⟹ τ S ⟹ τ T ⟹ τ (S ∩ T)`?
I avoid both of these at the top level of a formula. Instead, I use Isar
constructs: `assumes` and `shows` for lemma statements and `if` for the
introduction rules in inductive definitions.
> 5. In general, when should I use double quotation marks over
> cartouches if both options are available?
The default setting for PDF generation is to drop quotation marks but
preserve cartouches. Therefore, I use cartouches in precisely those
places where the bracketing they add may be necessary to understand the
code. In particular, I use quotation marks for propositions after things
like `lemma` and `have`, but I use cartouches around field types in
`datatype` declarations and locale arguments after `interpretation`.
Regarding my use of cartouches, consider something like the following:
datatype expr = App ‹expr ⇒ expr› ‹expr› | …
Dropping the cartouches would result in `expr ⇒ expr expr`, which would
look like there was only one field with this illegal type.
All the best,
This archive was generated by a fusion of
Pipermail (Mailman edition) and