Issues

• Soundness bug in mm0-c when using arrow form parameters

  digama0/mm0#214 · Filter by author sbp opened on Oct 25, 2026

• mm0-c: one .mm0 dummy can match two dummies of the .mmb definition [AI Pasta]

  digama0/mm0#213 · Filter by author zariuq opened on Oct 16, 2026

• Repeated declarations clobber old notations in mm0-c's parser

  digama0/mm0#210 · Filter by author gleachkr opened on Sep 22, 2026

• From MM to MM0, and vice-versa

  digama0/mm0#208 · Filter by author amelieled opened on Sep 15, 2026

• mm0-rs panic with def

  digama0/mm0#205 · Filter by author GinoGiotto opened on Jul 23, 2026
  1

• why mmc doesnt use linear types?

  digama0/mm0#204 · Filter by author srghma opened on May 29, 2026

• Proposal: add mm0-rs mm1-to-mm0 <input.mm1> [<output.mm0>] [--strip-comments] [--no-inline-imports]

  digama0/mm0#203 · Filter by author srghma opened on May 26, 2026
  1

• Proposal(ux): make sorts maximally limited by default

  digama0/mm0#202 · Filter by author srghma opened on May 26, 2026

• Proposal: levels of strict sorts

  digama0/mm0#201 · Filter by author srghma opened on May 25, 2026

• Deleted section still has reference

  digama0/mm0#199 · Filter by author icecream17 opened on May 5, 2026

• Spec typo?

  digama0/mm0#197 · Filter by author gleachkr opened on Apr 15, 2026
  1

• implement separation_logic.pdf in iris

  digama0/mm0#195 · Filter by author srghma opened on Mar 26, 2026

• Methods for expression reduction check and theorem-style substitution validation

  digama0/mm0#182 · Filter by author aethesia opened on Jan 12, 2026
  1

• mm0-rs panic

  digama0/mm0#178 · Filter by author GinoGiotto opened on Dec 27, 2025

• Pattern matching bug?

  digama0/mm0#177 · Filter by author GinoGiotto opened on Dec 23, 2025

• Feature Request: Support for Unicode Greek Letters in Variable Identifiers

  digama0/mm0#159 · Filter by author aethesia opened on Dec 2, 2025
  3

• have tactic should perform disjoint variable checks

  digama0/mm0#153 · Filter by author aethesia opened on Oct 27, 2025
  1

• mm0-rs - building a proc main with compiler.mm1

  digama0/mm0#152 · Filter by author Downchuck opened on Aug 6, 2025
  4

• Error handling

  digama0/mm0#125 · Filter by author uniwuni opened on May 13, 2023
  3

• Automatically generate the MM0 file from the MM1 file

  digama0/mm0#111 · Filter by author segf00lt opened on Oct 26, 2022
  3

• Using SMT-prover to generate proof

  digama0/mm0#80 · Filter by author j123123 opened on Apr 29, 2021
  3

• mm0 for kotlin

  digama0/mm0#78 · Filter by author Lakedaemon opened on Apr 15, 2021
  61

• mm0-ification of set.mm

  digama0/mm0#77 · Filter by author Lakedaemon opened on Apr 1, 2021
  1

• mm1 import cycles don't fail nicely

  digama0/mm0#49 · Filter by author ammkrn opened on Nov 16, 2020
  3

• mm0-rs as a library

  digama0/mm0#34 · Filter by author digama0 opened on Aug 4, 2020
  3