Also, I propose we add one lagda file for each section that contains code from all the snippets of that section but also type-checks (since not all snippets contain type-checkable Agda code). The current PR includes the first such file, called Section-1-1.lagda.
Add Agda snippets for Section 1.1.
Also, I propose we add one
lagdafile for each section that contains code from all the snippets of that section but also type-checks (since not all snippets contain type-checkable Agda code). The current PR includes the first such file, calledSection-1-1.lagda.