Commits

Commit history

1. Commits on Sep 27, 2026

   • feat: Add unsigned machine-integer induction as the kernel's fifteenth rule

     MattCCC

     committed
     3cb3ffaView commit details

     Copy full SHA for 3cb3ffa

     View code at this pointBrowse repository at this point
2. Commits on Sep 23, 2026

   • feat: Add falsity elimination so a checked contradiction closes a goal of any shape

     MattCCC

     committed
     b9bd5d5View commit details

     Copy full SHA for b9bd5d5

     View code at this pointBrowse repository at this point

   • docs: Point stale section citations at the sections that hold them

     MattCCC

     committed
     e6fe785View commit details

     Copy full SHA for e6fe785

     View code at this pointBrowse repository at this point
3. Commits on Sep 21, 2026

   • feat: decompose products and tagged sums through one structural provider

     MattCCC

     committed
     0903d64View commit details

     Copy full SHA for 0903d64

     View code at this pointBrowse repository at this point
4. Commits on Sep 20, 2026

   • feat: add kernel-checked disjunction propositions

     MattCCC

     committed
     d4f7fe1View commit details

     Copy full SHA for d4f7fe1

     View code at this pointBrowse repository at this point

   • chore: apply clang-tidy fixes across kernel, compiler, and tests

     MattCCC

     committed
     1084067View commit details

     Copy full SHA for 1084067

     View code at this pointBrowse repository at this point

   • feat: add kernel-checked conjunction propositions

     MattCCC

     committed
     0852358View commit details

     Copy full SHA for 0852358

     View code at this pointBrowse repository at this point

   • refactor: Format

     MattCCC

     committed
     ef7ac48View commit details

     Copy full SHA for ef7ac48

     View code at this pointBrowse repository at this point

   • feat: normalize machine arithmetic and check linear-arithmetic certificates

     MattCCC

     committed
     9d3d544View commit details

     Copy full SHA for 9d3d544

     View code at this pointBrowse repository at this point

   • feat(contracts): verify every return path of a branching body

     MattCCC

     committed
     10271fbView commit details

     Copy full SHA for 10271fb

     View code at this pointBrowse repository at this point

   • feat: Transform a goal with an established equality

     MattCCC

     committed
     5750221View commit details

     Copy full SHA for 5750221

     View code at this pointBrowse repository at this point

   • feat: Prove laws stated under a precondition

     MattCCC

     committed
     d72fd7eView commit details

     Copy full SHA for d72fd7e

     View code at this pointBrowse repository at this point
5. Commits on Sep 19, 2026

   • feat: Instantiate quantified evidence at a term

     MattCCC

     committed
     850c7a9View commit details

     Copy full SHA for 850c7a9

     View code at this pointBrowse repository at this point

   • feat: Add compiler spine with trusted proof kernel

     MattCCC

     committed
     f9ee3cdView commit details

     Copy full SHA for f9ee3cd

     View code at this pointBrowse repository at this point
6. Loading