Commit 2022-11-28 22:26 9dbb2a0b

feat: port linarith (#526) TODO:

• Before merge

• fix a bug in linarith in mathlib3 I just found ...
• depends on: #519
• style lint
• docs
• move theory stubs to a separate PR, for easier tracking: #733
• failing to parse the LinarithConfig option

• Before or after merge?

• Implement the removeNe preprocessor.
• Add support for restricting to a single type. How to store a Type in LinarithConfig?

• After merge

• Teach norm_num to solve example [LinearOrderedRing α] : (0 : α) < 37 := by norm_num.
• Port zify_proof (plumbing for zify), and add the natToInt preprocessor. Mostly done now, but see #741 before all the tests will work.
• Port cancel_denoms tactic, and add the cancelDenoms preprocessor.
• Add the nlinarith preprocessor and front-end syntax.