@@ -173,8 +173,10 @@ function back to itself. On such a path, there must be at least one
173argument which converges to a base case.
173argument which converges to a base case.
175- Mutually recursive functions are supported
175- Mutually recursive functions are supported
176- However, all functions on the path must be fully applied. In particular,
177- However, all functions on the path must be fully applied. In particular,
177 higher order applications are not supported
178 higher order applications are not supported
178- Idris identifies arguments which converge to a base case by looking for
180- Idris identifies arguments which converge to a base case by looking for
179 recursive calls to syntactically smaller arguments of inputs. e.g.
181 recursive calls to syntactically smaller arguments of inputs. e.g.
180 ``k`` is syntactically smaller than ``S (S k)`` because ``k`` is a
182 ``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
233flag, the IDRIS_LIB_DIR environment variable needs to be set to the path
235flag, the IDRIS_LIB_DIR environment variable needs to be set to the path
234where the Idris libs reside relative to the idris executable. The
236where the Idris libs reside relative to the idris executable. The
235IDRIS_TOOLCHAIN_DIR environment variable is optional, if that is set,
237IDRIS_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:
242+ IDRIS_LIB_DIR="./libs" \
243+ IDRIS_TOOLCHAIN_DIR="./mingw/bin" \
240− IDRIS_LIB_DIR="./libs" IDRIS_TOOLCHAIN_DIR="./mingw/bin" CABALFLAGS="-fffi -ffreestanding -frelease" make
244+ CABALFLAGS="-fffi -ffreestanding -frelease" \
243−What does the name ‘Idris’ mean?
248+What does the name “Idris” mean?
244================================
249================================
246British people of a certain age may be familiar with this
251British 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:
256- It's hard to type (this is important if you're using someone else's code, for
261- It's hard to type (this is important if you're using someone else's code, for
257 example). Various editors have their own input methods, but you have to know
262 example). Various editors have their own input methods, but you have to know
258 what they are.
263 what they are.
259- Not every piece of software easily supports it. Rendering issues have been
265- Not every piece of software easily supports it. Rendering issues have been
260 noted on some mobile email clients, terminal-based IRC clients, web browsers,
266 noted on some mobile email clients, terminal-based IRC clients, web browsers,
261 etc. There are ways to resolve these rendering issues but they provide a
267 etc. There are ways to resolve these rendering issues but they provide a
262 barrier to entry to using Idris.
268 barrier to entry to using Idris.
263- Even if we leave it out of the standard library (which we will in any case!)
270- Even if we leave it out of the standard library (which we will in any case!)
264 as soon as people start using it in their library code, others have to deal
271 as soon as people start using it in their library code, others have to deal
266- Too many characters look too similar. We had enough trouble with confusion
274- Too many characters look too similar. We had enough trouble with confusion
267 between 0 and O without worrying about all the different kinds of colons and
275 between 0 and O without worrying about all the different kinds of colons and
268 brackets.
276 brackets.
269- There seems to be a tendency to go over the top with use of Unicode. For
278- There seems to be a tendency to go over the top with use of Unicode. For
270 example, using sharp and flat for delay and force (or is it the other way
279 example, using sharp and flat for delay and force (or is it the other way
271 around?) in Agda seems gratuitous. We don't want to encourage this sort of
280 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
280Law <http://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.
289Law <http://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.
282This answer is based on Edwin Brady's response in the following
291This 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>`_.
285Where can I find the community standards for the Idris community?
294Where can I find the community standards for the Idris community?
286==================================================================
295==================================================================