The equation compiler and using_well_founded This page has moved to the leanprover-community website.