2023-01-20-lean_export.md

layout: post
author: frabe
title: "Lean Export in MMT"
tags:
  - Announcements

Starting with the most recent devel commit MMT includes an export of the Lean prover libraries (via the low-level export files as parsed by the treppline library.