.leanFrom the SWH-MSR-ARV dataset (Desmazières, Di Cosmo, Lorentz, MSR 2025; file nb_extensions_alphanum.csv) — one row per (ext, year) in the full SWH archive. Case-aggregated. citation.
Case variants in archive: .lean (1.0M), .Lean (55) — aggregated above.
This extension is attributed to Lean; Lean; Lean 4; Lean 4 as primary by 4 authoritative claims.
.lean among their extensions. Strength reflects whether the upstream source treated it as their primary extension.| Language | Source | Strength |
|---|---|---|
| Lean | linguist | primary |
| Lean | pygments | primary |
| Lean 4 | linguist | primary |
| Lean 4 | pygments | primary |
.lean on Wikidata
(property P1195) or in the Wikipedia infobox.
Source: data/derived/external_extension_index.csv.
Click Use as new PL on any row to open the
Add-PL form pre-filled with that entry's name, Wikipedia/Wikidata
URL, and this extension — one submission creates the PL + claim.
| Format | Class (Wikidata P31) | Suggested label | MIME | Notes | Action |
|---|---|---|---|---|---|
| Lean 3 file format Q130223835 file format | file format | — | text/x-lean; text/x-lean3 | — | Use as new PL ↗ |
| Lean 4 file format Q130224300 file format | file format | — | text/x-lean4 | — | Use as new PL ↗ |
| Lean file format family Q130225066 file format family | file format family | — | — | — | Use as new PL ↗ |
.lean file actually is.| Rule | Predicts | Kind | Predicates (truncated) |
|---|---|---|---|
h/linguist/.lean/0 | Lean | predicates | [{"kind": "any", "regexes": ["^import [a-z]"]}] |
h/linguist/.lean/1 | Lean 4 | predicates | [{"kind": "any", "regexes": ["^import [A-Z]"]}] |