Skip to content
Snippets Groups Projects
Normal view Permalink
2023-01-20-lean_export.md 373 B
Newer Older
  • Learn to ignore specific revisions
    • Florian Rabe's avatar
    no message
    Florian Rabe committed
    1 2 3 4 5 6 7 8 
    ---
layout: post
author: frabe
title: "Lean Export in MMT"
tags:
  - Announcements
---
Starting with [the most recent devel commit](https://github.com/UniFormal/MMT/commit/1c79ed7edff9ddf3af63073adaf5f33031cd0267) MMT includes an export of the Lean prover libraries (via the low-level export files as parsed by the [treppline](https://github.com/gebner/trepplein) library.