Repository navigation
Development notes
Marcus Zibrowius edited this page Sep 3, 2026
·
9 revisions
-
DONE Custom grind
-
DONE
Decide where to introduce grind in game. Keep tauto, ring, decide … . Don't keep linarith, omega. -
DONE
Refactor everything to do with inequalities and intervals, probably delete Luna. -
… probably some more refactoring necessary …
- Iso: add one ore two levels explaining concept of "equivalence"
-
New planets in the order described in the table below.
1st review, add Hints, 2nd review, add Branches, 3rd review … done.
(Next: add story, test with students, add translations …)
See folder Levels_inactive/v2
| name/content | status | picture |
|---|---|---|
| Analysis | ||
| Aquarium (bonuds & suprema) | done | |
| Shade (continuity) | done | |
| Slope (derivative) | done | exists: snail on pipe |
| Cartan (filters) | done | |
| Smooth_take-off [^1] | ready for 1st review | |
| Linear Algebra | ||
| Hamel (bump functions l.i.) | ||
| Terrace (step functions l.i.) | 2nd review | ?exists: mushrooms with flags? |
| MatrixSpan | ready for 1st review | |
| Quotients | ||
| SymmSquare | ready for 1st review | |
| Quotient: Finset/iso = Nat | ready for 1st review | |
| General | ||
| + RealUncountable | ready for 1st review | |
| Possible future versions: | ||
| +? FibresCard2 | WIP (Hint and Branch) | |
| Continuity | ||
| Epsilon-Delta-Differentiability | exists: ants | |
| Differentiability | exists: snail | |
| ContinuousFunction | ||
| CosExtInequality | ||
| Trash: | ||
| Tmp | ||
| VectorSpan | ||
| NewStuff | ||
| Quantum | ||
[^1]: Smooth take-off
- (ready for 1st review) simplify
Metadata/Induction.lean: probably only need a macro to read "induction" as "induction'" now that we haveDelaboratorNatSucc.lean. - (ready for 1st review) Iso: add one ore two levels explaining concept of "equivalence"