Commit 2026-11-10 13:17 9399e780

feat(Lean/Quote): restore Quote instances for Int and Rat (#44786) Add Quote Int and Quote Rat instances, analogous to core's Quote Nat. They turn a number into numeral syntax without a type ascription (e.g. quote (-7 / 2 : ℚ) is -7 / 2), so the result elaborates at the expected type. These could later be upstreamed to Lean core. These instances were added in #942 as part of polyrith, fixed in #24470, and removed together with the implementation of polyrith in #29547. This PR restores them unchanged (apart from naming) in their own file. Tests provided. Motivated from the project of maximize / minimize tactics (PR to follow) which print a computed rational bound in a "Try this" suggestion such as have : 4 * x + y ≤ 7 / 2 := by linarith. Discussed on Zulip: maximize / minimize tactic for linear optimization. The test file is refined with AI assistance (Claude) and has been reviewed by the author.