@@ -34,30 +34,22 @@ During elaboration TT (Raw) structure contains:
3434
3535For more information about holes and guesses see `Dependently Typed Functional Programs and their Proofs by McBride 1999`_.
3636
37−Type checker:
38−
39−- include universe levels
40−- distinguish between global and local bound names.
37+The following diagram is intended to illustrate a high level view of the tactics and how this eventually results in the TT language being generated. It is not necessary to understand the details at this stage. The intention is to help build up some intuition so that, when we get into the details, we can recognise how this fits into the big picture.
4138
4239.. image:: ../image/elabOverview.png
4340 :width: 410px
4441 :height: 282px
45− :alt: diagram illustrating TT language represented in a monad
46−
47−As already mentioned the TT core language is kept syntactically very simple. Part of the reason for this is that its correctness is already well proven using logic. For instance, here are the binders in TT with corresponding code and logic type introduction rules:
42+ :alt: diagram illustrating overview of TT language being generated from tactics.
4843
49−.. image:: ../image/binders.png
50− :width: 310px
51− :height: 203px
52− :alt: diagram illustrating basis of code in logic
44+As already mentioned the TT core language is kept syntactically very simple, for instance, here are the binders in TT with corresponding code and logic type introduction rules:
5345
5446.. list-table::
5547
56− * - There is an elaborator for both definitions and terms, the definition elaborator calls the term elaborator when required.
57− - .. image:: ../image/elab.png
58− :width: 141px
59− :height: 145px
60− :alt: diagram illustrating distinction between definition and term elaborator.
48+ * - This diagram illustrates the basis of the compilation process in logic (in this case for binders). It is not necessary to be an expert logician to understand elaborator reflection. However, when learning about tactics, they may appear arbitrary without knowing some theory.
49+ - .. image:: ../image/binders.png
50+ :width: 310px
51+ :height: 203px
52+ :alt: diagram illustrating basis of code in logic
6153
6254.. target-notes::
6355.. _`Edwin Brady's 2013 paper`: https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf