Commits

Commit history

1. Commits on Oct 5, 2026

   • fix: Test orderings with std::is_lt and std::is_neq so lint holds on every libstdc++

     MattCCC

     committed
     97037e7View commit details

     Copy full SHA for 97037e7

     View code at this pointBrowse repository at this point
2. 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
3. Commits on Sep 26, 2026

   • feat: Verify signed arithmetic, division and integer conversions with defined-behavior obligations

     MattCCC

     committed
     0e252ddView commit details

     Copy full SHA for 0e252dd

     View code at this pointBrowse repository at this point

   • feat: Add representability, truncating division and integer conversion primitives to the kernel

     MattCCC

     committed
     0256066View commit details

     Copy full SHA for 0256066

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

   • build: Require every translation unit and header to include what it uses

     MattCCC

     committed
     06495edView commit details

     Copy full SHA for 06495ed

     View code at this pointBrowse repository at this point

   • 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

   • chore: Drop the header includes nothing in those headers uses

     MattCCC

     committed
     4ff2077View commit details

     Copy full SHA for 4ff2077

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

   • feat: Add a kernel term former for indexed observation

     MattCCC

     committed
     1dfbcf5View commit details

     Copy full SHA for 1dfbcf5

     View code at this pointBrowse repository at this point

   • build: Run every GitHub CI environment locally from shared presets

     MattCCC

     committed
     3b4515fView commit details

     Copy full SHA for 3b4515f

     View code at this pointBrowse repository at this point

   • feat: Widen literals to the full machine range and decide exhaustive disjunctions

     MattCCC

     committed
     9d0960dView commit details

     Copy full SHA for 9d0960d

     View code at this pointBrowse repository at this point
6. 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
7. Commits on Sep 20, 2026

   • feat: add abstract values and checked logical projections

     MattCCC

     committed
     6c9b09cView commit details

     Copy full SHA for 6c9b09c

     View code at this pointBrowse repository at this point

   • 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

   • 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

   • feat: state universal and implication propositions feat: state universal and implication propositions forall (T x, ...) { P }` and `P -> Q`

     MattCCC

     committed
     3ac81dfView commit details

     Copy full SHA for 3ac81df

     View code at this pointBrowse repository at this point

   • feat: add Wno-pedantic flag

     MattCCC

     committed
     9786f4bView commit details

     Copy full SHA for 9786f4b

     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

   • fix: reject malformed core types

     MattCCC

     committed
     8f2ba63View commit details

     Copy full SHA for 8f2ba63

     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
8. 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
9. Loading