@@ -3,7 +3,7 @@ Generating Data and Functions at Compile Time
4We can construct a data structure at compile-time in an Elab monad.
4We can construct a data structure at compile-time in an Elab monad.
5This can allow proofs to be generated for user defined types or it could allow types to be automatically generated to support user defined types.
5This can allow proofs to be generated for user defined types or it could allow types to be automatically generated to support user defined types.
6−An example is the code, from <a href="https://dl.acm.org/citation.cfm?id=2951932">Christensen-Brady joint paper</a> ('Elaborator Reflection: Extending Idris in Idris'), that automatically generates accessibility predicates using the Bove-Capretta method.
6+An example is the code, from `Elaborator reflection: extending Idris in Idris`_, that automatically generates accessibility predicates using the Bove-Capretta method.
7The following simple outline example is adapted from
7The following simple outline example is adapted from
8`<https://github.com/idris-lang/Idris-dev/blob/master/test/meta002/DataDef.idr>`_
8`<https://github.com/idris-lang/Idris-dev/blob/master/test/meta002/DataDef.idr>`_
@@ -304,3 +304,5 @@ The above functions use the following data/records:
304 ||| The constructors for the family
304 ||| The constructors for the family
305 constructors : List (TTName, List CtorArg, Raw)</td>
305 constructors : List (TTName, List CtorArg, Raw)</td>
308+.. _`Elaborator reflection: extending Idris in Idris`: https://dl.acm.org/citation.cfm?doid=2951913.2951932