@@ -1,3 +1,8 @@
1+||| Primitives and tactics for elaborator reflection.
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.
1module Language.Reflection.Elab
6module Language.Reflection.Elab
3import Builtins
8import Builtins