idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.46k stars 369 forks source link

[ doc ] reference intro info on elab #3298

Closed jgarte closed 4 weeks ago

jgarte commented 4 weeks ago

Description

Hi,

I was not sure what elaborator reflection was and I saw references to it in the main docs but couldn't find any information introducing it.

This PR links introductory material by @stefan-hoeck as discussed with @buzden over Discord.