From 1df09b82a9458668324c8b448075af710ef6830d Mon Sep 17 00:00:00 2001 From: Li Xuanji Date: Fri, 7 Mar 2025 11:53:59 +0800 Subject: [PATCH 1/2] Add floor, ceil, min, max --- LeanTeXMathlib/Basic.lean | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/LeanTeXMathlib/Basic.lean b/LeanTeXMathlib/Basic.lean index cc98bde..7abbddd 100644 --- a/LeanTeXMathlib/Basic.lean +++ b/LeanTeXMathlib/Basic.lean @@ -130,3 +130,25 @@ latex_pp_app_rules (const := Finset.range) | _, #[hi] => do let hi ← latexPP hi return "[0, " ++ hi ++ ")" |>.resetBP .Infinity .Infinity + +latex_pp_app_rules (const := Nat.ceil) + | _, #[_, _, _, e] => do + let e ← LeanTeX.latexPP e + return "\\left\\lceil " ++ e ++ "\\right\\rceil" |>.resetBP .Infinity .Infinity + +latex_pp_app_rules (const := Nat.floor) + | _, #[_, _, _, e] => do + let e ← LeanTeX.latexPP e + return "\\left\\lfloor " ++ e ++ "\\right\\rfloor" |>.resetBP .Infinity .Infinity + +latex_pp_app_rules (const := Max.max) + | _, #[_, _, a, b] => do + let a ← LeanTeX.latexPP a + let b ← LeanTeX.latexPP b + return "\\max(" ++ a ++ "," ++ b ++ ")" |>.resetBP .Infinity .Infinity + +latex_pp_app_rules (const := Min.min) + | _, #[_, _, a, b] => do + let a ← LeanTeX.latexPP a + let b ← LeanTeX.latexPP b + return "\\min(" ++ a ++ "," ++ b ++ ")" |>.resetBP .Infinity .Infinity From 6db10ce5c13828b1bb03136b34a7b236ee850dd7 Mon Sep 17 00:00:00 2001 From: Li Xuanji Date: Fri, 7 Mar 2025 13:52:34 +0800 Subject: [PATCH 2/2] Add latex_pp_app_rules for const case --- LeanTeXMathlib/Basic.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/LeanTeXMathlib/Basic.lean b/LeanTeXMathlib/Basic.lean index 7abbddd..706a8b8 100644 --- a/LeanTeXMathlib/Basic.lean +++ b/LeanTeXMathlib/Basic.lean @@ -152,3 +152,8 @@ latex_pp_app_rules (const := Min.min) let a ← LeanTeX.latexPP a let b ← LeanTeX.latexPP b return "\\min(" ++ a ++ "," ++ b ++ ")" |>.resetBP .Infinity .Infinity + +latex_pp_app_rules (const := Singleton.singleton) + | _, #[_, _, _, a] => do + let a ← LeanTeX.latexPP a + return "\\{ " ++ a ++ " \\}" |>.resetBP .Infinity .Infinity