Document the Elab module itself
commitac26e38501d4bc4e5b056d93c6f96f74a00e2c83
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateSat 16 May 2015, 14:54 (11 years ago)
parent8826739
libs/prelude/Language/Reflection/Elab.idr+5
@@ -1,3 +1,8 @@
1+||| Primitives and tactics for elaborator reflection.
2+|||
3+||| Elaborator reflection allows Idris code to control Idris's
4+||| built-in elaborator, and re-use features like the unifier, the
5+||| type checker, and the hole mechanism.
16module Language.Reflection.Elab
27
38import Builtins