oops undo fie changed in error
commit75e2f824e7dcee3541915bf9f5316b7dae4e3923
authormartinbaker <git29f185@martinb.com>
dateFri 20 Dec 2019, 19:11 (7 years ago)
parentd74ca63
docs/reference/syntax-guide.rst+1−1
@@ -83,7 +83,7 @@ users of the module being written. This can be done using ``import public``:
8383
8484.. code-block:: idris
8585
86− # import public Data.Vect
86+ import public Data.Vect
8787
8888.. _syntax-variables:
8989