Metamath importer #176

Merged
merged 6 commits into from Aug 8, 2016

Conversation

Projects
None yet
2 participants
@digama0
Contributor

digama0 commented Aug 7, 2016

Ongoing work for the Metamath -> MMT import process.

  • Read .mm file
  • Parse the math grammar
  • Create MMT module declarations
  • Translate into LF statements

@Jazzpirate Jazzpirate merged commit 70dbf4f into UniFormal:master Aug 8, 2016

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment