Commits

Branch selector

 master

User selector

All users

All time

Commit History

Commits on Mar 23, 2026

• Wrong word

  achlipala

  committed
  03f6bc6

  Copy full SHA for 03f6bc6

• A more-interesting example of incomparable decidable theories, and change deployment method

  achlipala

  committed
  326d8b1

  Copy full SHA for 326d8b1

Commits on Dec 7, 2025

• Copyediting last chapters

  achlipala

  committed
  745f2f0

  Copy full SHA for 745f2f0

Commits on Nov 22, 2025

• Cite the newest chapter

  achlipala

  committed
  253166e

  Copy full SHA for 253166e

• Remove some dead code

  achlipala

  committed
  d1050e5

  Copy full SHA for d1050e5

Commits on Nov 16, 2025

• Add a template for Foundations

  achlipala

  committed
  8c74809

  Copy full SHA for 8c74809

• Cover a little bit about proof engines in the new chapter

  achlipala

  committed
  697dac1

  Copy full SHA for 697dac1

• Added Rocq code for the new chapter

  achlipala

  committed
  ab936db

  Copy full SHA for ab936db

• New chapter on type-theoretic foundations

  achlipala

  committed
  03e26f5

  Copy full SHA for 03e26f5

Commits on Nov 3, 2025

• Comment SymbolicExecution

  achlipala

  committed
  6cfdcbc

  Copy full SHA for 6cfdcbc

• SymbolicExecution: add a comment at the top

  achlipala

  committed
  cd23cc0

  Copy full SHA for cd23cc0

• SymbolicExecution: verifyP_computed

  achlipala

  committed
  fe2277a

  Copy full SHA for fe2277a

• SymbolicExecution: verifyM_computed

  achlipala

  committed
  596e3a6

  Copy full SHA for 596e3a6

• SymbolicExecution: verify_computed

  achlipala

  committed
  eea80aa

  Copy full SHA for eea80aa

Commits on Nov 2, 2025

• SymbolicExecution: verify_correct

  achlipala

  committed
  a46d14c

  Copy full SHA for a46d14c

• SymbolicExecution: somewhat manually proved a few examples using spost

  achlipala

  committed
  cddab3b

  Copy full SHA for cddab3b

• Merge branch 'symbolic-execution' of schizomaniac.net:git-root/frap into symbolic-execution

  achlipala

  committed
  a146863

  Copy full SHA for a146863

• Start of SymbolicExecution: proved spost_sound

  achlipala

  committed
  8ed6be8

  Copy full SHA for 8ed6be8

Commits on Oct 29, 2025

• Add AutomatedTheoremProving template

  achlipala

  committed
  df7730f

  Copy full SHA for df7730f

Commits on Oct 27, 2025

• Commented AutomatedTheoremProving

  achlipala

  committed
  687c632

  Copy full SHA for 687c632

Commits on Oct 25, 2025

• Broaden the example a bit

  achlipala

  committed
  4f5e656

  Copy full SHA for 4f5e656

Commits on Oct 21, 2025

• The example computed

  achlipala

  committed
  e5629df

  Copy full SHA for e5629df

• An example of the (baby) e-graph in action

  achlipala

  committed
  35027ba

  Copy full SHA for 35027ba

• Proved wpre_assertEqual

  achlipala

  committed
  38c6940

  Copy full SHA for 38c6940

Commits on Oct 19, 2025

• Proved the easier case of wpre_assertEqual

  achlipala

  committed
  5c51d0f

  Copy full SHA for 5c51d0f

• Factor out wpre_setLink

  achlipala

  committed
  2414d4d

  Copy full SHA for 2414d4d

• Proved wpre_checkEqual

  achlipala

  committed
  082bef9

  Copy full SHA for 082bef9

Commits on Oct 8, 2025

• AutomatedTheoremProving: finished wpre_checkEqual

  achlipala

  committed
  17ea05a

  Copy full SHA for 17ea05a

• AutomatedTheoremProving: much of wpre_checkEqual, but I realize the need to tweak the definition of 'rep'

  achlipala

  committed
  b6ec3d0

  Copy full SHA for b6ec3d0

Commits on Sep 27, 2025

• Start of a union-find e-graph-y example: proved path compression sound

  achlipala

  committed
  d0661e2

  Copy full SHA for d0661e2

Commits on Sep 21, 2025

• Copyediting

  achlipala

  committed
  d68d8f9

  Copy full SHA for d68d8f9

Commits on Sep 14, 2025

• Some copyediting

  achlipala

  committed
  4abaa03

  Copy full SHA for 4abaa03

Commits on Aug 20, 2025

• Bump copyright year

  achlipala

  committed
  68512ad

  Copy full SHA for 68512ad

• Updating for Rocq 9.0.0

  achlipala

  committed
  df53e19

  Copy full SHA for df53e19

Commits on Jun 6, 2024

• Italicize a term on first use (thanks to Todd Morley for the suggestion)

  achlipala

  committed
  55d128d

  Copy full SHA for 55d128d