@@ -34,30 +34,22 @@ During elaboration TT (Raw) structure contains:
35For more information about holes and guesses see `Dependently Typed Functional Programs and their Proofs by McBride 1999`_.
35For more information about holes and guesses see `Dependently Typed Functional Programs and their Proofs by McBride 1999`_.
37−Type checker:
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.
39−- include universe levels
40−- distinguish between global and local bound names.
42.. image:: ../image/elabOverview.png
39.. image:: ../image/elabOverview.png
43 :width: 410px
40 :width: 410px
44 :height: 282px
41 :height: 282px
45− :alt: diagram illustrating TT language represented in a monad
42+ :alt: diagram illustrating overview of TT language being generated from tactics.
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:
49−.. image:: ../image/binders.png
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:
52− :alt: diagram illustrating basis of code in logic
54.. list-table::
46.. list-table::
56− * - There is an elaborator for both definitions and terms, the definition elaborator calls the term elaborator when required.
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.
57− - .. image:: ../image/elab.png
49+ - .. image:: ../image/binders.png
58− :width: 141px
50+ :width: 310px
59− :height: 145px
51+ :height: 203px
60− :alt: diagram illustrating distinction between definition and term elaborator.
52+ :alt: diagram illustrating basis of code in logic
62.. target-notes::
54.. target-notes::
63.. _`Edwin Brady's 2013 paper`: https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf
55.. _`Edwin Brady's 2013 paper`: https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf