Commit 2023-05-16 10:59 a6e1045f

View on Github →

chore: reenable eta, bump to nightly 2023-05-16 (#3414) Now that leanprover/lean4#2210 has been merged, this PR:

  • removes all the set_option synthInstance.etaExperiment true commands (and some etaExperiment% term elaborators)
  • removes many but not quite all set_option maxHeartbeats commands
  • makes various other changes required to cope with leanprover/lean4#2210.

Estimated changes

modified theorem Polynomial.C_eq_int_cast
modified def Lagrange.interpolate