Maybe we should think of the structure of our Guide. Examples that I think are good: - [Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean/) - [Arend Tutorial](https://arend-lang.github.io/documentation/tutorial) - [PLFA Part 1](https://plfa.github.io/) is actually the best resource I've ever seen for learning entry-level Agda.
Maybe we should think of the structure of our Guide. Examples that I think are good: