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

9 lines
157 B
JavaScript
Executable File

export default {
name: 'Lean',
type: 'programming',
aceMode: 'text',
extensions: ['.lean', '.hlean'],
languageId: 197,
tmScope: 'source.lean',
}