mseri / BET

Project for "Machine-Checked Mathematics" at the Lorentz Center
Apache License 2.0
6 stars 5 forks source link

Removed the "find_home"s for better compilation time. #61

Closed D-Thomine closed 2 weeks ago

D-Thomine commented 2 weeks ago

The find_homes took too much time to run. I took their returns, put them in comment, and removed them.

Note: these comments are not definitive recommendations, but merely the results of find_home.

Some minor formatting (replacing bad dots by good dots...).

mseri commented 2 weeks ago

Thanks