Skip to content

Commit 01c2898

Browse files
Post-merge cleanup of PR #1
- Remove .codex-gitconfig: Windows-specific Codex tooling artifact accidentally bundled with the contribution; not project state. - Drop Loop space stanza from Riemannian.lean public API list. The file and import are retained; names (BasedLoop, FreeLoop, LoopInterval) are not yet committed as stable surface pending iteration over Mathlib.Topology.Path. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent cc78a96 commit 01c2898

2 files changed

Lines changed: 0 additions & 16 deletions

File tree

.codex-gitconfig

Lines changed: 0 additions & 10 deletions
This file was deleted.

Riemannian.lean

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -103,12 +103,6 @@ intermediate identities) are internal and may change without notice.
103103
* `Riemannian.manifoldGradientNormSq`
104104
* `Riemannian.manifoldGradient_riesz`
105105
106-
**Loop space** (`LoopSpace.lean`):
107-
* `Riemannian.LoopInterval`
108-
* `Riemannian.BasedLoop`, `Riemannian.LoopSpace`
109-
* `Riemannian.FreeLoop`, `Riemannian.FreeLoopSpace`
110-
* `Riemannian.BasedLoop.const`, `Riemannian.FreeLoop.const`
111-
112106
**Bump functions** (`BumpFunction.lean`):
113107
* `OpenGALib.BumpFunction.expDamping`
114108
* `OpenGALib.BumpFunction.smoothStep`

0 commit comments

Comments
 (0)