We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent c7f5688 commit 01f2d3fCopy full SHA for 01f2d3f
1 file changed
README.md
@@ -78,21 +78,5 @@ lake build
78
`lake build` is wired up as a CI check via
79
`.github/workflows/lean_action_ci.yml`.
80
81
-## File layout
82
83
-```
84
-.
85
-├── Archimedean.lean — the entire portfolio file (~130 lines)
86
-├── lakefile.toml — Mathlib pinned at v4.29.1
87
-├── lean-toolchain — leanprover/lean4:v4.29.1
88
-└── README.md
89
90
-
91
-## Author
92
93
-Riccardo Borsetto, PhD student at the University of Verona (Logic
94
-Group). Research focus: Higher Observational Type Theory, Cubical
95
-Agda, and the constructive foundations of analysis.
96
97
-Cubical Agda contributions: see the open PRs and the TYPES 2026
98
-abstract above.
0 commit comments