diff --git a/LeanTeXMathlib/Basic.lean b/LeanTeXMathlib/Basic.lean index c9849ba..2337516 100644 --- a/LeanTeXMathlib/Basic.lean +++ b/LeanTeXMathlib/Basic.lean @@ -126,6 +126,44 @@ latex_pp_app_rules (const := Finset.Ioi) let lo ← latexPP lo return "(" ++ lo ++ ", \\infty)" |>.resetBP .Infinity .Infinity +latex_pp_app_rules (const := Set.Icc) + | _, #[_, _, lo, hi] => do + let lo ← latexPP lo + let hi ← latexPP hi + return "[" ++ lo ++ ", " ++ hi ++ "]" |>.resetBP .Infinity .Infinity +latex_pp_app_rules (const := Set.Ico) + | _, #[_, _, lo, hi] => do + let lo ← latexPP lo + let hi ← latexPP hi + return "[" ++ lo ++ ", " ++ hi ++ ")" |>.resetBP .Infinity .Infinity +latex_pp_app_rules (const := Set.Ioc) + | _, #[_, _, lo, hi] => do + let lo ← latexPP lo + let hi ← latexPP hi + return "(" ++ lo ++ ", " ++ hi ++ "]" |>.resetBP .Infinity .Infinity +latex_pp_app_rules (const := Set.Ioo) + | _, #[_, _, lo, hi] => do + let lo ← latexPP lo + let hi ← latexPP hi + return "(" ++ lo ++ ", " ++ hi ++ ")" |>.resetBP .Infinity .Infinity + +latex_pp_app_rules (const := Set.Iio) + | _, #[_, _, hi] => do + let hi ← latexPP hi + return "(-\\infty, " ++ hi ++ ")" |>.resetBP .Infinity .Infinity +latex_pp_app_rules (const := Set.Iic) + | _, #[_, _, lo] => do + let lo ← latexPP lo + return "(-\\infty, " ++ lo ++ "]" |>.resetBP .Infinity .Infinity +latex_pp_app_rules (const := Set.Ici) + | _, #[_, _, lo] => do + let lo ← latexPP lo + return "[" ++ lo ++ ", \\infty)" |>.resetBP .Infinity .Infinity +latex_pp_app_rules (const := Set.Ioi) + | _, #[_, _, lo] => do + let lo ← latexPP lo + return "(" ++ lo ++ ", \\infty)" |>.resetBP .Infinity .Infinity + latex_pp_app_rules (const := Finset.range) | _, #[hi] => do let hi ← latexPP hi @@ -158,6 +196,17 @@ latex_pp_app_rules (const := Singleton.singleton) let a ← LeanTeX.latexPP a return "\\{ " ++ a ++ " \\}" |>.resetBP .Infinity .Infinity +latex_pp_app_rules (const := Inv.inv) + | _, #[_, _, a] => do + let a ← LeanTeX.latexPP a + return a.protectRight 100 ++ LatexData.atomString "^{-1}" + +latex_pp_app_rules (const := HSMul.hSMul) + | _, #[_, _, _, _, a, b] => do + let a ← LeanTeX.latexPP a + let b ← LeanTeX.latexPP b + return "(" ++ a ++ " \\cdot " ++ b ++ ")" |>.resetBP .Infinity .Infinity + latex_pp_app_rules (const := DirectSum) | _, #[ι, β, _inst] => do let pι ← withExtraSmallness 2 <| latexPP ι @@ -181,4 +230,3 @@ 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) - diff --git a/test/basic.lean b/test/basic.lean index 67990dc..141131d 100644 --- a/test/basic.lean +++ b/test/basic.lean @@ -60,6 +60,34 @@ latex_pp_app_rules (kind := any) (paramKinds := params) #texify Real.arcsin (Real.cos 2) + +/-- info: (0, \frac{\pi}{2}) -/ +#guard_msgs in #latex Set.Ioo 0 (Real.pi / 2) + +/-- info: [0, \frac{\pi}{2}) -/ +#guard_msgs in #latex Set.Ico 0 (Real.pi / 2) + +/-- info: (0, \frac{\pi}{2}] -/ +#guard_msgs in #latex Set.Ioc 0 (Real.pi / 2) + +/-- info: [0, \frac{\pi}{2}] -/ +#guard_msgs in #latex Set.Icc 0 (Real.pi / 2) + +/-- info: (-\infty, 5) -/ +#guard_msgs in #latex Set.Iio 5 + +/-- info: (-\infty, 5] -/ +#guard_msgs in #latex Set.Iic 5 + +/-- info: [5, \infty) -/ +#guard_msgs in #latex Set.Ici 5 + +/-- info: (5, \infty) -/ +#guard_msgs in #latex Set.Ioi 5 + +/-- info: 3^{-1} -/ +#guard_msgs in #latex (3:ℝ)⁻¹ + open scoped DirectSum #texify ⨁ i, (Fin i → ℝ)