Skip to content

15th Git Release

Choose a tag to compare

View all tags
@Jazzpirate Jazzpirate released this 18 Dec 21:25
· 2167 commits to master since this release
v15.0.0
b75848a
  • IDE Improvements
    • Support for the MMT Plugin for the IntelliJ-IDE
    • added a Scala console to JEdit to interact with MMT’s internal classes from within jEdit
  • New examples in MMT/examples
    • resource semantics of linear logic (logic/linear.mmt)
    • prototypical theorem prover (logic/prover.mmt)
    • proof irrelevance as a logical feature (logic/pl.mmt)
    • inductive functions on lists as special cases of rewrite rules (lists.mmt)
    • case study on implicit morphisms: lattice of theories of regular bands
  • New Concrete link syntax
    • for includes that include a morphism expression as opposed to an MMT URI
  • Added support for right-associative delimiters in mixfix notations
    • Use %Rd for delimiter d that associates to the right
  • Cleanups and additions to various internal components
    • first steps towards implicit coercions
    • new class DocumentLevel (e.g., archive, folder, file, theory, etc.); every document now carries it level
    • new elementEnd calls after processing container elements in all MMT components
    • dropped distinction between declared and defined elements, container elements now inherit from ModuleOrLink class
    • re-implemented applicability check of checking rules
    • various cleanups of the MathHub API
  • compatible with major reimplementations of archives:
    • LFX
    • MitM/Foundation
    • MitM/smglom
Assets 3
Loading