Code

Prove derive_commutes#132

Code

Merged

awalterschulze merged 3 commits intokatydid:mainkatydid/regex-deriv-lean:mainfrom keeganperry7:derive_commuteskeeganperry7/katydid-proofs:derive_commutesCopy head branch name to clipboardJan 13, 2025

+88-2

Commits

Commits on Jan 11, 2025

• Prove derive_commutes

  keeganperry7

  committed
  b420c16

  Copy full SHA for b420c16

Commits on Jan 12, 2025

• Simplify proof

  keeganperry7

  committed
  31831b5

  Copy full SHA for 31831b5

• Replace constructor with Iff.intro

  keeganperry7

  committed
  4feaec6

  Copy full SHA for 4feaec6