Skip to content

Fix(lean,#24019): en-tetes EN i18n perimes apres le merge de #23931 #24070

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
myia-ai-01 merged 2 commits into from
Nov 2, 2026
Merged

Fix(lean,#24019): en-tetes EN i18n perimes apres le merge de #23931 #24070

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9f6ca92
Fix(lean,#24019): en-tetes EN i18n perimes apres le merge de #23931
jsboige Nov 1, 2026
ed4de22
Fix(lean,#24019): en-tetes EN -- enoncer la regle d'import, pas le ro…
jsboige Nov 1, 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
11 changes: 6 additions & 5 deletions MyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Folk_en.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,11 +24,12 @@ import Mathlib.Topology.Basic
EN historique pré-Option A à recover, fichier FR-first depuis origin).

Namespace sibling : `RepeatedGames_en` (the FR canonical stays
`RepeatedGames`). Shared types `PrisonersDilemma`, `PDAction` (defined in
`Stage.lean` under `namespace RepeatedGames`) are re-exposed via
`open RepeatedGames` so the EN sibling resolves them as FR `GrimTrigger_en`
does. Field projections `g.P`/`g.R`/`g.S`/`g.T` are structure-field access
(not namespace dot-notation), hence safe under the open.
`RepeatedGames`). Shared types `PrisonersDilemma`, `PDAction` are defined
in `Stage_en.lean` under `namespace RepeatedGames_en` and consumed via
`import RepeatedGames.Stage_en`; every higher-level EN sibling of this
series resolves them through `open RepeatedGames_en`. Field
projections `g.P`/`g.R`/`g.S`/`g.T` are structure-field access
(not namespace dot-notation), hence unaffected by the open.

See #4980. Part of #4208 (axe E).
-/
Expand Down
15 changes: 10 additions & 5 deletions MyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Stage_en.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,11 +16,16 @@ import Mathlib.Tactic
Namespace: `RepeatedGames_en` (anti-collision with `RepeatedGames` of
the FR canonical `Stage.lean`). External access:
`RepeatedGames_en.PDAction`, `RepeatedGames_en.PrisonersDilemma`, etc.
No external module imports this EN sibling; the FR-canonical modules
(Discounting, GrimTrigger, Folk) reference `RepeatedGames.PrisonersDilemma`
via `open RepeatedGames` (the FR namespace), and the higher-level EN
siblings (Discounting_en, GrimTrigger_en) likewise reference the FR
base types. This Stage_en is the autonomous EN mirror of the foundation.
Import rule for this series: every higher-level EN module imports
`RepeatedGames.Stage_en` and works inside `namespace RepeatedGames_en`,
resolving the base types through `open RepeatedGames_en`, never through
the FR namespace. The current roster of those modules is the
`## Structure` section of `RepeatedGames_en.lean`; it is deliberately not
restated here, so adding a sibling means updating one place, not two.
The FR-canonical modules (Discounting, GrimTrigger, Folk) stay inside
`namespace RepeatedGames` and reference the base types directly, and no
FR module crosses into the EN namespace. This Stage_en is the autonomous
EN mirror of the foundation.

Methodological note: manual translation of the FR canonical (no historical
pre-Option-A EN source to recover; FR-first file since origin).
Expand Down
Loading