Skip to content

Commit 17a3e65

Browse files
kmillkmill
committed
Moved LeanTeX pretty printers here that depend on mathlib
1 parent e10c164 commit 17a3e65

4 files changed

Lines changed: 220 additions & 1 deletion

File tree

‎LeanTeXMathlib/Basic.lean‎

Lines changed: 53 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1,53 @@
1-
def hello := "world"
1+
import LeanTeX
2+
import Mathlib
3+
4+
/-!
5+
# LaTeX pretty printers for mathlib
6+
7+
-/
8+
9+
open LeanTeX
10+
11+
namespace Mathlib.LeanTeX
12+
13+
open Lean
14+
open scoped MkAppNMacro
15+
16+
-- Note: `HasSubset.Subset` is not in scope here
17+
latex_pp_app_rules (const := HasSubset.Subset)
18+
| _, #[_, _, a, b] => do
19+
let a ← latexPP a
20+
let b ← latexPP b
21+
return a.protectRight 50 ++ LatexData.nonAssocOp " \\subseteq " 50 ++ b.protectLeft 50
22+
23+
@[latex_pp_app const.Union.union] def pp_Union := basicBinOpPrinter " \\cup " 65 .left 4
24+
@[latex_pp_app const.Inter.inter] def pp_Inter := basicBinOpPrinter " \\cap " 70 .left 4
25+
26+
/-- This renders `Set.image f X` as `f[X]`, which is a reasonably common notation for set image. -/
27+
latex_pp_app_rules (const := Set.image)
28+
| _, #[_, _, f, X] => do
29+
let f ← latexPP f
30+
let X ← latexPP X
31+
return ← f.protectRight funAppBP ++ X.brackets |>.mergeBP (lbp := .NonAssoc funAppBP) (rbp := .NonAssoc funAppBP)
32+
|>.maybeWithTooltip s!"image of \\({X.latex.1}\\) under \\({f.latex.1}\\)"
33+
34+
latex_pp_app_rules (const := Finset.prod)
35+
| _, #[_α, _β, _inst, s, f] => do
36+
let set ← withExtraSmallness 2 <| latexPP s
37+
withBindingBodyUnusedName' f `i fun name body => do
38+
let pbody ← latexPP body
39+
let pbody := pbody.protectLeft 66
40+
let psum := (← (LatexData.atomString "\\prod" |>.bigger 1).sub (s!"{name.toLatex} \\in " ++ set) |>.maybeWithTooltip "Finset.prod") ++ pbody
41+
return psum |>.resetBP (lbp := .Infinity) |>.mergeBP (rbp := .NonAssoc 65)
42+
43+
latex_pp_app_rules (const := Finset.sum)
44+
| _, #[_α, _β, _inst, s, f] => do
45+
let set ← withExtraSmallness 2 <| latexPP s
46+
withBindingBodyUnusedName' f `i fun name body => do
47+
let pbody ← latexPP body
48+
let pbody := pbody.protectLeft 66
49+
let psum := (← (LatexData.atomString "\\sum" |>.bigger 1).sub (s!"{name.toLatex} \\in " ++ set) |>.maybeWithTooltip "Finset.sum") ++ pbody
50+
return psum |>.resetBP (lbp := .Infinity) |>.mergeBP (rbp := .NonAssoc 65)
51+
52+
latex_pp_const_rule Rat := (LatexData.atomString "\\mathbb{Q}").maybeWithTooltip "Rat"
53+
latex_pp_const_rule Real := (LatexData.atomString "\\mathbb{R}").maybeWithTooltip "Real"

‎lake-manifest.json‎

Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
{"version": "1.1.0",
2+
"packagesDir": ".lake/packages",
3+
"packages":
4+
[{"url": "https://github.com/kmill/LeanTeX",
5+
"type": "git",
6+
"subDir": null,
7+
"scope": "kmill",
8+
"rev": "3bd8c91e567269609a0ad6ec9eaf04da3bb4fe08",
9+
"name": "LeanTeX",
10+
"manifestFile": "lake-manifest.json",
11+
"inputRev": "main",
12+
"inherited": false,
13+
"configFile": "lakefile.lean"},
14+
{"url": "https://github.com/leanprover-community/mathlib4",
15+
"type": "git",
16+
"subDir": null,
17+
"scope": "leanprover-community",
18+
"rev": "a69bc35b7028de551fb3c101d72f5ddbef2a6b2d",
19+
"name": "mathlib",
20+
"manifestFile": "lake-manifest.json",
21+
"inputRev": "master",
22+
"inherited": false,
23+
"configFile": "lakefile.lean"},
24+
{"url": "https://github.com/leanprover-community/ProofWidgets4",
25+
"type": "git",
26+
"subDir": null,
27+
"scope": "leanprover-community",
28+
"rev": "a602d13aca2913724c7d47b2d7df0353620c4ee8",
29+
"name": "proofwidgets",
30+
"manifestFile": "lake-manifest.json",
31+
"inputRev": "v0.0.53",
32+
"inherited": true,
33+
"configFile": "lakefile.lean"},
34+
{"url": "https://github.com/leanprover-community/batteries",
35+
"type": "git",
36+
"subDir": null,
37+
"scope": "leanprover-community",
38+
"rev": "092b30de8e7ee78e96b24c235d99e26f2942d77e",
39+
"name": "batteries",
40+
"manifestFile": "lake-manifest.json",
41+
"inputRev": "v4.18.0-rc1",
42+
"inherited": true,
43+
"configFile": "lakefile.toml"},
44+
{"url": "https://github.com/leanprover-community/plausible",
45+
"type": "git",
46+
"subDir": null,
47+
"scope": "leanprover-community",
48+
"rev": "ebfb31672ab0a5b6d00a018ff67d2ec51ed66f3a",
49+
"name": "plausible",
50+
"manifestFile": "lake-manifest.json",
51+
"inputRev": "main",
52+
"inherited": true,
53+
"configFile": "lakefile.toml"},
54+
{"url": "https://github.com/leanprover-community/LeanSearchClient",
55+
"type": "git",
56+
"subDir": null,
57+
"scope": "leanprover-community",
58+
"rev": "0c169a0d55fef3763cfb3099eafd7b884ec7e41d",
59+
"name": "LeanSearchClient",
60+
"manifestFile": "lake-manifest.json",
61+
"inputRev": "main",
62+
"inherited": true,
63+
"configFile": "lakefile.toml"},
64+
{"url": "https://github.com/leanprover-community/import-graph",
65+
"type": "git",
66+
"subDir": null,
67+
"scope": "leanprover-community",
68+
"rev": "08372f1ec11df288ff76621ead7b0b575cb29355",
69+
"name": "importGraph",
70+
"manifestFile": "lake-manifest.json",
71+
"inputRev": "main",
72+
"inherited": true,
73+
"configFile": "lakefile.toml"},
74+
{"url": "https://github.com/leanprover-community/aesop",
75+
"type": "git",
76+
"subDir": null,
77+
"scope": "leanprover-community",
78+
"rev": "ec060e0e10c685be8af65f288e23d026c9fde245",
79+
"name": "aesop",
80+
"manifestFile": "lake-manifest.json",
81+
"inputRev": "master",
82+
"inherited": true,
83+
"configFile": "lakefile.toml"},
84+
{"url": "https://github.com/leanprover-community/quote4",
85+
"type": "git",
86+
"subDir": null,
87+
"scope": "leanprover-community",
88+
"rev": "d892d7a88ad0ccf748fb8e651308ccd13426ba73",
89+
"name": "Qq",
90+
"manifestFile": "lake-manifest.json",
91+
"inputRev": "master",
92+
"inherited": true,
93+
"configFile": "lakefile.toml"},
94+
{"url": "https://github.com/leanprover/lean4-cli",
95+
"type": "git",
96+
"subDir": null,
97+
"scope": "leanprover",
98+
"rev": "dd423cf2b153b5b14cb017ee4beae788565a3925",
99+
"name": "Cli",
100+
"manifestFile": "lake-manifest.json",
101+
"inputRev": "main",
102+
"inherited": true,
103+
"configFile": "lakefile.toml"}],
104+
"name": "LeanTeX_Mathlib",
105+
"lakeDir": ".lake"}

‎lakefile.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ package "LeanTeX_Mathlib" where
1010
]
1111

1212
require "leanprover-community" / "mathlib"
13+
require "kmill" / "LeanTeX"
1314

1415
@[default_target]
1516
lean_lib «LeanTeXMathlib» where

‎test/basic.lean‎

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
import LeanTeXMathlib
2+
import Lean.Elab.Tactic.Guard
3+
4+
set_option linter.unusedVariables false
5+
6+
open Lean
7+
8+
def a : Nat := 22
9+
10+
open Real LeanTeX in
11+
latex_pp_const_rule Real.pi := LatexData.atomString "\\pi" |>.maybeWithTooltip "real.pi"
12+
13+
def f : Nat → Nat → Nat := λ x y => x + y
14+
15+
def g : Unit → Nat := λ _ => 22
16+
17+
variable (b : Nat) (s : Finset Nat) (t : Nat → Finset Nat) (c : Nat → Real → Real) (x : Real)
18+
19+
/-- info: \sum_{x \in s}(x + 1) -/
20+
#guard_msgs in #latex s.sum (λ x => x + 1)
21+
/-- info: \sum_{x \in s}2 \cdot x -/
22+
#guard_msgs in #latex s.sum (λ x => 2 * x)
23+
/-- info: \left(\sum_{x \in s}(x + 1)\right) \cdot \text{a} -/
24+
#guard_msgs in #latex s.sum (λ x => x + 1) * a
25+
/-- info: \text{a} \cdot \sum_{x \in s}(x + 1) -/
26+
#guard_msgs in #latex a * s.sum (λ x => x + 1)
27+
/-- info: \left(\sum_{x \in s}(x + 1)\right) + \text{a} -/
28+
#guard_msgs in #latex s.sum (λ x => x + 1) + a
29+
/-- info: \text{a} + \sum_{x \in s}(x + 1) -/
30+
#guard_msgs in #latex a + s.sum (λ x => x + 1)
31+
/-- info: \left(\sum_{x \in s}(x + 1)\right) \cdot \sum_{x \in s}2 \cdot x -/
32+
#guard_msgs in #latex s.sum (λ x => x + 1) * s.sum (λ x => 2 * x)
33+
/-- info: (c : \mathbb{N}) \mapsto c \cdot \sum_{x \in s}\sum_{y \in t_{x}}x \cdot y -/
34+
#guard_msgs in #latex λ (c : Nat) => c * s.sum (λ x => (t x).sum (λ y => x * y))
35+
/-- info: \sum_{i \in s}\text{id}(i) -/
36+
#guard_msgs in #latex s.sum id
37+
38+
open LeanTeX in
39+
/-- An experiment: use a subscript for an argument. Represents `Fin n` as `\mathbb{N}_{<n}` -/
40+
-- TODO make work for multi-argument like Nat → Nat → Real → Real
41+
latex_pp_app_rules (kind := any) (paramKinds := params)
42+
| f, #[n] => do
43+
if params[0]!.bInfo.isExplicit && params[0]!.type.isConstOf `Nat then
44+
let f ← latexPP f
45+
let n ← withExtraSmallness 2 <| latexPP n
46+
return f.sub n
47+
else
48+
failure
49+
50+
/-- info: (f : \mathbb{N} \to \mathbb{N}) \mapsto \left(\sum_{i \in s}f_{i}\right)^{2} -/
51+
#guard_msgs in #latex λ (f : Nat → Nat) => (s.sum f)^2
52+
53+
#texify s.sum (λ x => x + 1)
54+
#texify s.sum (λ x => 2 * x)
55+
#texify s.sum (λ x => x + 1) * a
56+
#texify a * s.sum (λ x => x + 1)
57+
#texify s.sum (λ x => x + 1) + a
58+
#texify a + s.sum (λ x => x + 1)
59+
#texify s.sum (λ x => x + 1) * s.sum (λ x => 2 * x)
60+
#texify λ (c : Nat) => c * s.sum (λ x => (t x).sum (λ y => x * y))
61+
#texify s.sum id

0 commit comments

Comments
 (0)