Code

chore: remove fin_destr tactic#13

Code

Merged

alexkeizer merged 5 commits intomasteralexkeizer/QpfTypes:masterfrom remove-findestralexkeizer/QpfTypes:remove-findestrCopy head branch name to clipboardMay 20, 2024

+101-187

Commits

Commits on May 20, 2024

• chore: prove PFin2 is equivalent to Fin2

  alexkeizer

  committed
  2683495

  Copy full SHA for 2683495

• chore: eliminate some uses of fin_destr

  alexkeizer

  committed
  461dc6f

  Copy full SHA for 461dc6f

• chore: remove use of fin_destr in Sum.lean

  alexkeizer

  committed
  3215baa

  Copy full SHA for 3215baa

• chore: remove final use of fin_destr in data macro

  alexkeizer

  committed
  2a5ed3d

  Copy full SHA for 2a5ed3d

• chore: delete fin_destr code

  alexkeizer

  committed
  602c40e

  Copy full SHA for 602c40e