Add formal scoping model appendix

This adds the Agda model for describing our rules for extending
temporary scopes (originally by dianne) as a [literate Agda] file
included in the Reference appendix.

To the original Agda formulation, I've added a proof of equivalence
between two models, an introduction, and a reading guide for Rust
users.

This appendix is still is rough shape.  This is just a draft.  There's
no syntax highlighting yet for the Agda code; we're not yet checking
that the Agda code compiles in CI; the chapter compares stable Rust to
a PR, but we instead need to present the PR behavior as the adopted
behavior; etc.  This commit is published just for discussion and
revision.

[literate Agda]: https://agda.readthedocs.io/en/latest/tools/literate-programming.html

Co-authored-by: dianne <diannes.gm@gmail.com>

Author: traviscross

.gitignore

@@ -1,2 +1,3 @@
+*.agdai
 /book
 /target

src/SUMMARY.md

@@ -135,6 +135,7 @@
     - [Grammar summary](grammar.md)
     - [Syntax index](syntax-index.md)
     - [Macro follow-set ambiguity formal specification](macro-ambiguity.md)
+    - [Formal scoping model](scoping-model.lagda.md)
     - [Influences](influences.md)
     - [Test summary](test-summary.md)
     - [Glossary](glossary.md)