Add floor, ceil, min, max, singleton

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)
+