[[LeanNote idioms/Table of Contents#Overview|Overview]] | idiom | Description | Effects the goal | Effects a hypotheses | | -------------------- | ------------------------------------------------------------------------ | :--------------: | :------------------: | | [[apply-relabeling]] | Correct the mislabeled conclusion term after applying Modus Ponens. | | ⎷ | | [[exact-show]] | Provide explicit term : type information to close a proof. | ⎷ | | | [[intro-typing]] | Provide explicit term : type information when a goal premise is assumed. | ⎷ | ⎷ | | | | | | ## Overview Many programming languages that begin as untyped eventually provide a `strictly typed` mode, to provide a safer programming style that is also more self-explanatory. Lean is already a strictly typed language, but it's exceptional ability to infer types can lead to code that is difficult for the human reader to understand. The `LeanNote idioms` define a coding style is easier for the non-advanced Lean coder to understand. It provides: - explicit type information whenever practical - a naming convention that errors on the side of elaboration. - a commenting style provides context to a line of code when its meaning is not immediately clear. - code substitutions that clear up to obfuscated Lean effects. See [[apply-relabeling]].