Commit 2026-10-21 16:48 91cc66b8

chore: deprecate FP.Float (#44425) This PR deprecates FP.Float. This definition is very poorly documented, has not been touched since the port, and says it is experimental. Nowadays, lean core has a Float type with the ability to prove things about it, so I think it's better to remove FP.Float. This PR is motivated by a new concrete instances linter. The parameter [C : FloatCfg] appearing in this file causes this linter to warn.