Re: [isabelle] Several questions about coding style/best practices


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 MHonArc.