Skip to content

Adding lean4 as language #31

@AnirudhG07

Description

@AnirudhG07

Hi, Thanks for the amazing streamlit code editor. I would like to add lean4 as a language in the option lang, which is currently not there as it seems.
The community has made highlightjs-lean. Can you pls share on how to add this language for lang? Please share what other resources might be needed to get it to work.
The react-syntax-highlighter repo seems unmaintained so this issue has yet to be resolved.

Thanks in advance!

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions