All pull requests

Pull requests

• Name a datatype's SMT parameters from its own binders (fixes #454)

  #455·logicalmechanism opened Nov 3, 2026·4 tasks done·

  ·

• solver optimization: avoid unnecessary list value construction on List operators and add new simplification rules

  #446·etiennejf opened Oct 29, 2026Collaborator·

  ·

• Prototype typed counterexample reconstruction and ToCEX export

  #445·RSoulatIOHK opened Oct 29, 2026Collaborator·

  ·

• Emit proof steps for the String literal folds and order rules

  #444·felipeperet opened Oct 28, 2026Collaborator·11 of 21 tasks·

  ·

• Emit the premise proofs of the forall rules that reduce to True

  #443·felipeperet opened Oct 27, 2026Collaborator·12 of 21 tasks·

  ·

• Replay String.append steps in their ++ spelling

  #442·felipeperet opened Oct 27, 2026Collaborator·11 of 21 tasks·

  ·

• [Lean 4.35 7/7] Document supported semantics and downstream migration

  #439·RSoulatIOHK opened Oct 27, 2026Collaborator·

  ·

• [Lean 4.35 4/7] Prepare character normalization and dependent proofs on Lean 4.24

  #438·RSoulatIOHK opened Oct 27, 2026Collaborator·

  ·

• [Lean 4.35 3/7] Prepare constructor-field reduction on Lean 4.24

  #437·RSoulatIOHK opened Oct 27, 2026Collaborator·

  ·

• [Lean 4.35 2/7] Prepare checked recursive models on Lean 4.24

  #436·RSoulatIOHK opened Oct 27, 2026Collaborator·

  ·

• feat(cli): compiler-style counterexample diagnostics

  #435·RSoulatIOHK opened Oct 27, 2026Collaborator·

  ·

• [Lean 4.35 6/7] Support polymorphic string replacement with faithful SMT semantics

  #434·RSoulatIOHK opened Oct 27, 2026Collaborator·

  ·

• [Lean 4.35 5/7] Migrate compiler APIs, String views and fixtures together

  #432·RSoulatIOHK opened Oct 27, 2026Collaborator·

  ·

• [Lean 4.35 1/7] Pin CI toolchains and preserve build failures

  #431·RSoulatIOHK opened Oct 27, 2026Collaborator·

  ·

• feat(cli): add installable lean-blaster executable with bundled Z3

  #424·RSoulatIOHK opened Oct 26, 2026Collaborator·8 tasks done·

  ·

• Add maintainer-triggered generic issue-fix bot

  #415·RSoulatIOHK opened Oct 23, 2026Collaborator·

  ·
  2

• Fix constructor equality across equivalent universe levels

  #414·RSoulatIOHK opened Oct 23, 2026Collaborator·8 of 10 tasks·

  ·
  1

• Finite-field CVC5 Integration [DRAFT]

  #412·Riley-Kilgore opened Oct 23, 2026Member·12 of 21 tasks·

  ·

• Emit proof steps for the BEq rules and the BEq to Eq bridge

  #411·felipeperet opened Oct 22, 2026Collaborator·11 of 21 tasks·

  ·

• 352 elaborate the testoptimize input once so the proof gate maps anonymous instance binders

  #408·MarcoNardell1 opened Oct 21, 2026Collaborator·6 of 21 tasks·

  ·

• Soundness: only canonical LT/LE instances and instance arguments of function values

  #368·SeungheonOh opened Oct 21, 2026·

  ·
  1

• Experiment with deferred constructor match propagation

  #366·RSoulatIOHK opened Oct 20, 2026Collaborator·

  ·

• Publish PR benchmark results from isolated workflow

  #365·RSoulatIOHK opened Oct 20, 2026Collaborator·

  ·

• Balance the four PR benchmark runners

  #364·RSoulatIOHK opened Oct 20, 2026Collaborator·

  ·

• chore(benchmark): weekly results update

  #360·github-actions[bot] opened Oct 19, 2026Bot·

  ·