ent\":{\"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\"]}"))

export default [
lang
]