import "./chunk-DWU6NC2D.js";

// ../node_modules/.pnpm/@shikijs+langs@2.1.0/node_modules/@shikijs/langs/dist/lean.mjs
var lang = Object.freeze(JSON.parse(`{"displayName":"Lean 4","fileTypes":[],"name":"lean","patterns":[{"include":"#comments"},{"match":"\\\\b(Prop|Type|Sort)\\\\b","name":"storage.type.lean4"},{"match":"\\\\battribute\\\\b\\\\s*\\\\[[^\\\\]]*\\\\]","name":"storage.modifier.lean4"},{"match":"@\\\\[[^\\\\]]*\\\\]","name":"storage.modifier.lean4"},{"match":"\\\\b(?<!\\\\.)(global|local|scoped|partial|unsafe|private|protected|noncomputable)(?!\\\\.)\\\\b","name":"storage.modifier.lean4"},{"match":"\\\\b(sorry|admit|stop)\\\\b","name":"invalid.illegal.lean4"},{"match":"#(print|eval|reduce|check|check_failure)\\\\b","name":"keyword.other.lean4"},{"match":"\\\\bderiving\\\\s+instance\\\\b","name":"keyword.other.command.lean4"},{"begin":"\\\\b(?<!\\\\.)(inductive|coinductive|structure|theorem|axiom|abbrev|lemma|def|instance|class|constant)\\\\b\\\\s+(\\\\{[^}]*\\\\})?","beginCaptures":{"1":{"name":"keyword.other.definitioncommand.lean4"}},"end":"(?=\\\\bwith\\\\b|\\\\bextends\\\\b|\\\\bwhere\\\\b|[:\\\\|\\\\(\\\\[\\\\{⦃<>])","name":"meta.definitioncommand.lean4","patterns":[{"include":"#comments"},{"include":"#definitionName"},{"match":","}]},{"match":"\\\\b(?<!\\\\.)(theorem|show|have|from|suffices|nomatch|def|class|structure|instance|set_option|initialize|builtin_initialize|example|inductive|coinductive|axiom|constant|universe|universes|variable|variables|import|open|export|theory|prelude|renaming|hiding|exposing|do|by|let|extends|mutual|mut|where|rec|syntax|macro_rules|macro|deriving|fun|section|namespace|end|infix|infixl|infixr|postfix|prefix|notation|abbrev|if|then|else|calc|match|with|for|in|unless|try|catch|finally|return|continue|break)(?!\\\\.)\\\\b","name":"keyword.other.lean4"},{"begin":"«","contentName":"entity.name.lean4","end":"»"},{"begin":"(s!)\\"","beginCaptures":{"1":{"name":"keyword.other.lean4"}},"end":"\\"","name":"string.interpolated.lean4","patterns":[{"begin":"(\\\\{)","beginCaptures":{"1":{"name":"keyword.other.lean4"}},"end":"(\\\\})","endCaptures":{"1":{"name":"keyword.other.lean4"}},"patterns":[{"include":"$self"}]},{"match":"\\\\\\\\[\\\\\\\\\\"ntr']","name":"constant.character.escape.lean4"},{"match":"\\\\\\\\x[0-9A-Fa-f][0-9A-Fa-f]","name":"constant.character.escape.lean4"},{"match":"\\\\\\\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]","name":"constant.character.escape.lean4"}]},{"begin":"\\"","end":"\\"","name":"string.quoted.double.lean4","patterns":[{"match":"\\\\\\\\[\\\\\\\\\\"ntr']","name":"constant.character.escape.lean4"},{"match":"\\\\\\\\x[0-9A-Fa-f][0-9A-Fa-f]","name":"constant.character.escape.lean4"},{"match":"\\\\\\\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]","name":"constant.character.escape.lean4"}]},{"match":"\\\\b(true|false)\\\\b","name":"constant.language.lean4"},{"match":"'[^\\\\\\\\']'","name":"string.quoted.single.lean4"},{"captures":{"1":{"name":"constant.character.escape.lean4"}},"match":"'(\\\\\\\\(x[0-9A-Fa-f][0-9A-Fa-f]|u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]|.))'","name":"string.quoted.single.lean4"},{"match":"\`+[^\\\\[(]\\\\S+","name":"entity.name.lean4"},{"match":"\\\\b([0-9]+|0([xX][0-9a-fA-F]+)|[-]?(0|[1-9][0-9]*)(\\\\.[0-9]+)?([eE][+-]?[0-9]+)?)\\\\b","name":"constant.numeric.lean4"}],"repository":{"blockComment":{"begin":"/-","end":"-/","name":"comment.block.lean4","patterns":[{"include":"source.lean4.markdown"},{"include":"#blockComment"}]},"comments":{"patterns":[{"include":"#dashComment"},{"include":"#docComment"},{"include":"#stringBlock"},{"include":"#modDocComment"},{"include":"#blockComment"}]},"dashComment":{"begin":"--","end":"$","name":"comment.line.double-dash.lean4","patterns":[{"include":"source.lean4.markdown"}]},"definitionName":{"patterns":[{"match":"\\\\b[^:«»\\\\(\\\\)\\\\{\\\\}[:space:]=→λ∀?][^:«»\\\\(\\\\)\\\\{\\\\}[:space:]]*","name":"entity.name.function.lean4"},{"begin":"«","contentName":"entity.name.function.lean4","end":"»"}]},"docComment":{"begin":"/--","end":"-/","name":"comment.block.documentation.lean4","patterns":[{"include":"source.lean4.markdown"},{"include":"#blockComment"}]},"modDocComment":{"begin":"/-!","end":"-/","name":"comment.block.documentation.lean4","patterns":[{"include":"source.lean4.markdown"},{"include":"#blockComment"}]}},"scopeName":"source.lean4","aliases":["lean4"]}`));
var lean_default = [
  lang
];
export {
  lean_default as default
};
//# sourceMappingURL=lean-H7G6LQKK.js.map