git.iko.soy/Idris-dev
on master help sign in
update reference section
d74ca63martinbaker
docs/reference/index.rst−1
compare with master
unifiedsplit
@@ -36,7 +36,6 @@ This will tell you how Idris works, for using it you should read the Idris Tutor
36 internals
36 internals
37 language-features
37 language-features
38 language-extensions
38 language-extensions
39− elaborator-reflection
40 type-directed-search
39 type-directed-search
41 partial-evaluation
40 partial-evaluation
42 misc
41 misc
docs/reference/syntax-guide.rst+1−1
@@ -83,7 +83,7 @@ users of the module being written. This can be done using ``import public``:
83
83
84.. code-block:: idris
84.. code-block:: idris
85
85
86− import public Data.Vect
86+ # import public Data.Vect
87
87
88.. _syntax-variables:
88.. _syntax-variables:
89
89