Files
rspade_system/node_modules/linguist-languages/data/Lean_20_4.js
2025-12-03 21:28:08 +00:00

10 lines
175 B
JavaScript
Executable File

module.exports = {
name: 'Lean 4',
type: 'programming',
aceMode: 'text',
extensions: ['.lean'],
languageId: 455147478,
tmScope: 'source.lean4',
group: 'Lean',
}