on master help sign in
Document the Elab module itself
ac26e38David Raymond Christiansen
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.
1module Language.Reflection.Elab
6module Language.Reflection.Elab
2
7
3import Builtins
8import Builtins