Commit 2023-02-06 22:14 52c04a34

feat: require @[simps!] if simps runs in expensive mode (#1885)

• This does not change the behavior of simps, just raises a linter error if you run simps in a more expensive mode without writing !.
• Fixed some incorrect occurrences of to_additive, simps. Will do that systematically in future PR.
• Fix port of OmegaCompletePartialOrder.ContinuousHom.ofMono a bit