Code

Simp rfl thm#32

Code

Draft

tobiasgrosser wants to merge 8 commits intomasteropencompl/lean4:masterfrom simp_rfl_thmopencompl/lean4:simp_rfl_thmCopy head branch name to clipboard

+254-53

Commits

Commits on Jul 18, 2024

• feat: Simp.Config.implicitDefEqProofs

  leodemoura

  committed
  9177efa

  Copy full SHA for 9177efa

• chore: fix tests

  leodemoura

  committed
  f06f161

  Copy full SHA for f06f161

• fix: use implicitDefEqProofs := true at split tactic

  leodemoura

  committed
  b79a1da

  Copy full SHA for b79a1da

• chore: missing trace[split.failure]

  leodemoura

  committed
  63ea6f5

  Copy full SHA for 63ea6f5

• fix: do not look for split-tactic candidates in proof terms

  Show description for 57bc19f
  leodemoura

  committed
  57bc19f

  Copy full SHA for 57bc19f

• fix: split candidate selection

  leodemoura

  committed
  f66e0db

  Copy full SHA for f66e0db

Commits on Jul 19, 2024

• chore: fix tests

  leodemoura

  committed
  9702909

  Copy full SHA for 9702909

Commits on Nov 1, 2024

• Merge commit '0fcee100e7ea382069854d91e854265c56b54428' into simp_rfl_thm

  tobiasgrosser

  committed
  513b2f2

  Copy full SHA for 513b2f2