BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Marcus Rossel
DTSTART:20250116T173000Z
DTEND:20250116T180000Z
DTSTAMP:20260414T201906Z
UID:LeanTogether2025/22
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2025/22/">Egg: An Equality Saturation Tactic in Lean</a>\nby Marcus Rossel
  as part of Lean Together 2025\n\n\nAbstract\nRewriting is an extremely co
 mmon proof task supported by efficient and versatile tactics like $\\textt
 t{rw}$ and $\\texttt{simp}$. These tactics are\, however\, limiting in tha
 t users need to either provide an explicit order and direction of rewrites
 \, or rely on a fixed simplification direction. In our talk\, we present a
  new (work in progress) tactic for rewriting using equality saturation. Th
 is approach allows us to tackle goals which are infeasible for $\\texttt{s
 imp}$ without requiring the details needed for $\\texttt{rw}$.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/22/
END:VEVENT
END:VCALENDAR