@@ -173,8 +173,10 @@ function back to itself. On such a path, there must be at least one
173173argument which converges to a base case.
174174
175175- Mutually recursive functions are supported
176+
176177- However, all functions on the path must be fully applied. In particular,
177178 higher order applications are not supported
179+
178180- Idris identifies arguments which converge to a base case by looking for
179181 recursive calls to syntactically smaller arguments of inputs. e.g.
180182 ``k`` is syntactically smaller than ``S (S k)`` because ``k`` is a
@@ -233,14 +235,17 @@ where the install directory is unknown at build time. When passing this
233235flag, the IDRIS_LIB_DIR environment variable needs to be set to the path
234236where the Idris libs reside relative to the idris executable. The
235237IDRIS_TOOLCHAIN_DIR environment variable is optional, if that is set,
236−Idris will use that path to find the C compiler.
238+Idris will use that path to find the C compiler. For example:
237239
238−Example::
240+::
239241
240− IDRIS_LIB_DIR="./libs" IDRIS_TOOLCHAIN_DIR="./mingw/bin" CABALFLAGS="-fffi -ffreestanding -frelease" make
242+ IDRIS_LIB_DIR="./libs" \
243+ IDRIS_TOOLCHAIN_DIR="./mingw/bin" \
244+ CABALFLAGS="-fffi -ffreestanding -frelease" \
245+ make
241246
242247
243−What does the name ‘Idris’ mean?
248+What does the name “Idris” mean?
244249================================
245250
246251British people of a certain age may be familiar with this
@@ -256,16 +261,20 @@ There are several reasons why we should not support Unicode operators:
256261- It's hard to type (this is important if you're using someone else's code, for
257262 example). Various editors have their own input methods, but you have to know
258263 what they are.
264+
259265- Not every piece of software easily supports it. Rendering issues have been
260266 noted on some mobile email clients, terminal-based IRC clients, web browsers,
261267 etc. There are ways to resolve these rendering issues but they provide a
262268 barrier to entry to using Idris.
269+
263270- Even if we leave it out of the standard library (which we will in any case!)
264271 as soon as people start using it in their library code, others have to deal
265272 with it.
273+
266274- Too many characters look too similar. We had enough trouble with confusion
267275 between 0 and O without worrying about all the different kinds of colons and
268276 brackets.
277+
269278- There seems to be a tendency to go over the top with use of Unicode. For
270279 example, using sharp and flat for delay and force (or is it the other way
271280 around?) in Agda seems gratuitous. We don't want to encourage this sort of
@@ -280,7 +289,7 @@ This seems like an instance of `Wadler's
280289Law <http://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.
281290
282291This answer is based on Edwin Brady's response in the following
283−`pull request <https://github.com/idris-lang/Idris-dev/pull/694#issuecomment-29559291>`__.
292+`pull request <https://github.com/idris-lang/Idris-dev/pull/694#issuecomment-29559291>`_.
284293
285294Where can I find the community standards for the Idris community?
286295==================================================================