mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-10-26 09:54:23 +03:00
add links between sections
This commit is contained in:
parent
4abb58f13c
commit
25af56b26b
@ -198,7 +198,12 @@ This is primarily useful for code generation, particularly for generating patter
|
||||
|
||||
Learn More
|
||||
==========
|
||||
Tactics are discussed in the proofs section.
|
||||
|
||||
Some tactics are introduced in the :ref:`proofs-index` section with further details, of those most relevant to elaborator reflection, on the following pages.
|
||||
|
||||
The list of built-in tactics can be obtained using the ``:browse`` command in an Idris REPL or the corresponding feature in one of the graphical IDE clients to explore the ``Language.Reflection.Elab.Tactics`` namespace.
|
||||
All of the built-in tactics contain documentation strings.
|
||||
|
||||
For alternative ways to extend the Idris language see the :ref:`reference-index` section.
|
||||
|
||||
The following pages explain more about the theory and practice of elaborator reflection.
|
||||
|
@ -3,7 +3,6 @@ Language Extensions
|
||||
*******************
|
||||
|
||||
|
||||
|
||||
Type Providers
|
||||
===============
|
||||
|
||||
@ -34,3 +33,9 @@ repository <https://github.com/david-christiansen/idris-type-providers>`__.
|
||||
More detailed descriptions are available in David Christiansen's `WGP
|
||||
'13 paper <http://dx.doi.org/10.1145/2502488.2502495>`__ and `M.Sc.
|
||||
thesis <http://itu.dk/people/drc/david-christiansen-thesis.pdf>`__.
|
||||
|
||||
Elaborator Reflection
|
||||
=====================
|
||||
|
||||
Another way to extend the language is elaborator reflection which is described
|
||||
in the :ref:`elaborator-index` section.
|
||||
|
Loading…
Reference in New Issue
Block a user