## Summary
The [[LeanNotes coding style - Overview|LeanNotes coding style]] attempts to provide a gentler first exposure to the concepts that make Lean such a powerful proof assistant. The `LeanNote style` provides:
- explicit type information whenever practical.
- a naming convention that errors on the side of elaboration.
- a commenting style that provides a before and after context for tactic applications..
- code substitutions that clear up to obfuscated Lean effects. See the [[Ln-apply-relabeled-tactic]].
## LeanNotes-tactics (Ln-tactic)
LEanNotes tactics are listed in the Tactics section, they have a prefix that distinguishes them: `Ln-tactic`
| Idiom | Description | Effects the goal | Effects a hypotheses |
| ----------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------ | :--------------: | :------------------: |
| [[Ln-apply-relabeled-tactic\|apply-relabeled]] | Correct the mislabeled conclusion term after applying Modus Ponens. | | ⎷ |
| [[Ln-exact-show-tactic\|exact-show]] | Provide explicit term : type information to close a proof. | ⎷ | |
| [[Ln-intro-typing-tactic\|intro-typing]] | Provide explicit term : type information when a goal premise is assumed. | ⎷ | ⎷ |
## Other topics
| Topic | Description |
| ----------------------------------------------------------------------------------------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| [[AI prompts]] | This wiki note includes my generic prompt that is included in .lean files as the first comment. It has proved useful for code that has errors or confusing syntax. |
| [[File header template]] | All LeanNote .lean files include a customized version of this header template. The key piece of information is the URL to a LeanNotes wiki note associated with the .lean file that includes annotations, copyright information, author credits and a README section. |
| [[]] | This wiki notes defines which letters are commonly used for various types. |
| | |
| | |
---
**`LeanNotes curator:`** [[dducoff]], [Contact dducoff](https://tally.so/r/rjQYWL)
**`Posted Date`**: 2026-08-15