diff --git a/LeanTeXMathlib/Basic.lean b/LeanTeXMathlib/Basic.lean index b246596..c9849ba 100644 --- a/LeanTeXMathlib/Basic.lean +++ b/LeanTeXMathlib/Basic.lean @@ -131,6 +131,33 @@ latex_pp_app_rules (const := Finset.range) 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 + +latex_pp_app_rules (const := Singleton.singleton) + | _, #[_, _, _, a] => do + let a ← LeanTeX.latexPP a + return "\\{ " ++ a ++ " \\}" |>.resetBP .Infinity .Infinity + latex_pp_app_rules (const := DirectSum) | _, #[ι, β, _inst] => do let pι ← withExtraSmallness 2 <| latexPP ι @@ -154,3 +181,4 @@ latex_pp_app_rules (const := PiTensorProduct) let pbody ← latexPP body let psum := (← (LatexData.atomString "\\bigotimes" |>.bigger 1).sub (s!"{name.toLatex} \\in " ++ pι) |>.maybeWithTooltip "PiTensorProduct") ++ pbody return psum |>.resetBP (rbp := .NonAssoc 0) +