# Hypotheses Names ## Naming guidelines - Hypothesis have an "h" prefix. - Binary boolean connectives, `∧`, `∨`, `→`, `↔`, are spelled out as in: - P ∧ Q :`hPandQ`, P ∨ Q : `hPorQ`, P → Q :`hPimpliesQ`, P ↔ Q : `hPiffQ` - The boolean negation operator, `¬` is spelled out in an underbar prefix, which provides separation from other lowercase spellings: - ¬P : `h_notP`, ¬¬P : `h_not_notP`, P ∨ ¬P : `Por_notP` - Parentheses are mapped to pairs of underbars as in: - `(P → Q) → R` : `_PimpliesQ_R`, ((P ∧ Q) ∨ R) : `h__PandQ_orR)` - When a boolean expression is too complex to be named with the above rules, then it is named by either: - a numbering scheme as in: `h1`, `h2`, ..., `h<n>` - its logical or mathematical role as in: `hPremise`, `hConclusion`, `hContrapositive`, `h_f_is_continuous` ## Naming examples | term | maps to | hypothesis | Comment | | ---------------------------- | ------- | ------------------------------- | ------------------------------------------------------------------------------------------------------------------- | | P | | `hP` | Use P, Q, R, S, T as Prop constant terms | | ¬P | | `h_notP` | Negation is mapped to a not prefix. | | P ∧ Q | | `hPandQ` | | | P ∨ Q | | `hPorQ` | | | P → Q | | `hPimpliesQ` | Clarity as the expense of wordyness. | | P → (Q → R) | | `hPimplies_QimpliesR_` | The implication arrow maps to juxtaposition. | | P ↔ Q | | `hPiffQ` | | | P ↔ (Q ↔ R) | | `hPiff_QiffR_` | | | | | | | | P ∨ ¬Q | | `hPor_notQ` | Parentheses are mapped to underbars. Note that the underbar prefix in `_not` separates it from the `or` connective. | | (¬P ∨ Q) ∧ R | | `h_PorQ_andR` | Parentheses are mapped to underbars. | | | | | | | Complex hypotheses | | `hPremise`, `h_f_is_continuous` | A complex hypothesis spelling describes it math or logic role. | | Multiple lengthly hypothesis | | `h1`, `h2`, ..., `h<n>` | Multiple complex hypothesis are numbered. | # Unused constants have an underbar prefix followed a clear tactic Use an underbar prefix followed by an identifier to designate an unused identifier. Then apply yhe [[clear-tactic| clear]] tactic to remove it from the infoview. The point here is to remove clutter. **Notes**: - The Lean parser recognizes both _ and \_{identifier} as an unused identifier. - The `set_option linter.unusedVariables false` directive can be used to turn off linter warnings of unused identifiers, but a better approach is to use the [[clear-tactic|clear]] tactic. # Shadowed identifiers have single quote suffixes When an identifier is shadowed, use one or more single quotes, ', to designate the shadow identifiers These shadow identifiers are not used in subsequent portions within the current context; only the first (non-shadow) identifier is used. **Examples**: - if the term *hP* has one shadow, then the shadow is named *\_hp* - If the term hP has more than one shadow, then the shadows are enumerated by quote suffixes as in: *\_hp', \_hp'', \_hp'''*. - The shadowed versions of the original constant, \_hp', and \_hp'' , are not used in subsequent portions within the current context. That is, the original identifier, hP, is the only spelling used in subsequent occurrences within the current context. **Rationale**: The Lean syntax allows shadowed constants to be referred to implicitly with no name in the code and only as a reference in the infoview. An underbar placeholder and also be used for shadowed constants. Both of these syntax conventions can require backwards code scanning to remember which variable is being shadowed. This backward scanning can be avoided by using this style guideline. Example: ```lean theorem pPPPP : P → P → P → P := by intros hP hP' hP'' -- ⊢ P sorry ``` ![[Shadowed term example.png]]