Skip to content
Closed
Changes from 1 commit
Commits
Show all changes
40 commits
Select commit Hold shift + click to select a range
28680c5
chore: add tests for binary and higher-order products
grunweg Oct 12, 2025
a02c199
refactor: if we found a model with corners on a normed or inner produ…
grunweg Jan 24, 2026
2d92b44
refactor: split findModel into an inner and outer loop
grunweg Jan 24, 2026
4b47782
feat: support arbitrary combinations of products, disjoint unions and…
grunweg Jan 24, 2026
64d95cf
Update tests: products now work
grunweg Jan 24, 2026
f984c21
Add tests for sums, open sets and interaction.
grunweg Jan 24, 2026
2cd5dad
chore: uncomment two previous tests for products
grunweg Jan 24, 2026
db40db5
chore: reorder for more coherent flow
grunweg Jan 24, 2026
9e0c003
refactor: introduce an abbrev for the normed space information
grunweg Jan 24, 2026
74a6b97
chore: introduce another abbreviation for the output of findModelInner
grunweg Jan 24, 2026
9d37275
Update module doc-strings accordingly
grunweg Jan 24, 2026
efa6c28
chore: restore previous error message
grunweg Jan 28, 2026
2503339
Fix typo
grunweg Jan 28, 2026
959a14c
wip: debugging opens failures
grunweg Jan 28, 2026
728fd4e
Revert "wip: debugging opens failures"
grunweg Jan 29, 2026
6e14f10
Merge branch 'master' into diffgeo-custom-elaborators-products-binary
grunweg Jan 29, 2026
02abf14
chore: refactor a bit
thorimur Jan 31, 2026
c4745cd
chore: tweak message?
thorimur Jan 31, 2026
24bcaf8
fix: don't use `s!`, postpone constructing error message until necessary
thorimur Jan 31, 2026
1c96c68
chore: update test for new trace message
thorimur Jan 31, 2026
4f73925
chore: remove `tryStrategy'` TODO :)
thorimur Jan 31, 2026
3700422
fix: don't derive `Repr` to satisfy unusedArguments linter?
thorimur Jan 31, 2026
24b08ae
Remove duplicate code
grunweg Jan 31, 2026
9686919
Documentation tweaks
grunweg Jan 31, 2026
0c8c17f
Debugging output
grunweg Jan 31, 2026
2fd5eb1
Tweak
grunweg Jan 31, 2026
5fec4d2
fix: match branch for `Subtype` coercion
thorimur Feb 11, 2026
28afd96
Make the opens branch do something useful
grunweg Feb 11, 2026
2e7ae73
Tweaks
grunweg Feb 11, 2026
a0dea35
Merge branch 'master' into diffgeo-custom-elaborators-products-binary
grunweg Feb 12, 2026
3f286c3
Merge branch 'master' into diffgeo-custom-elaborators-products-binary
grunweg Feb 18, 2026
bd8db5f
chore: clean up `isCLMReduciblyDefeqCoefficients`
thorimur Feb 18, 2026
74fc876
Update Mathlib/Geometry/Manifold/Notation.lean
grunweg Feb 18, 2026
a9222d9
Update Mathlib/Geometry/Manifold/Notation.lean
grunweg Feb 18, 2026
1a5d967
Better documentation; tweak trace message
grunweg Feb 18, 2026
68def9b
Bless test change: let's wait on the dependent PR!
grunweg Feb 18, 2026
4955331
Merge branch 'master' into diffgeo-custom-elaborators-products-binary
grunweg Feb 19, 2026
1cb9bef
fixup; TODO audit test change!
grunweg Feb 19, 2026
4e6b42a
Fix merge: keep this copy instead!
grunweg Feb 19, 2026
b8cbf1f
Apply suggestions from code review
grunweg Feb 19, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
chore: remove tryStrategy' TODO :)
  • Loading branch information
thorimur committed Jan 31, 2026
commit 4f73925bd361a4429afedf50e81f1a7df2581170
1 change: 0 additions & 1 deletion Mathlib/Geometry/Manifold/Notation.lean
Original file line number Diff line number Diff line change
Expand Up @@ -235,7 +235,7 @@
normedSpace : Expr
/-- The expression for the normed space's base field. -/
baseField : Expr
deriving Repr, Inhabited

Check failure on line 238 in Mathlib/Geometry/Manifold/Notation.lean

View workflow job for this annotation

GitHub Actions / Build (fork)

Manifold.Elab.instReprNormedSpaceInfo.repr argument 2 prec✝ : ℕ

/--
Information about a model with corners found through search.
Expand All @@ -252,12 +252,11 @@
/-- Information on the underlying normed space if this model it the trivial model with corners on
a normed space. -/
normedSpaceInfo? : Option NormedSpaceInfo := none
deriving Repr, Inhabited

Check failure on line 255 in Mathlib/Geometry/Manifold/Notation.lean

View workflow job for this annotation

GitHub Actions / Build (fork)

Manifold.Elab.instReprFindModelResult.repr argument 2 prec✝ : ℕ

instance : Coe Expr FindModelResult where
coe model := { model }

-- TODO: deduplicate with tryStrategy', somehow!
/-- Try a strategy `x : TermElabM` which either successfully produces some `Expr` or fails. On
failure in `x`, exceptions are caught, traced (`trace.Elab.DiffGeo.MDiff`), and `none` is
successfully returned.
Expand Down
Loading