Zulip Chat Archive

Stream: lean4

Topic: MIME type for Lean 4 source code files


Raghuram (Jun 22 2025 at 13:04):

Is there a MIME type file for Lean 4 source code files? I'm trying to set a default application for opening .lean files and it seems like I need this to apply a default to just those instead of all text files.

Raghuram (Jun 22 2025 at 13:24):

In case it isn't, here's a very basic one people may find useful:

<?xml version="1.0" encoding="UTF-8"?>
<mime-info xmlns="http://www.freedesktop.org/standards/shared-mime-info">
    <mime-type type="text/x-lean4">
        <comment>Lean 4 source code</comment>
        <sub-class-of type="text/plain"/>
        <glob pattern="*.lean"/>
    </mime-type>
</mime-info>

Last updated: Dec 20 2025 at 21:32 UTC