Port Haskell's Bounded class

This is useful for avoiding magic numbers.
Split Bounded into lower and upper bound type classes
Total order on Nat
Add minimum and maximum on newly defined Order class
Order on Fin
Documentation improvement
Decidable instance for FinLTE
Evaluator bug fix

Weakening out of scope variables should not happen (we had a flawed
assumption about where the evaluator might be called from...)
Fix include for sockaddr_in and initialization of addr in idrnet_sockaddr_ipv4
Parser warnings; especially for invalid doc comments

This patch adds:

 * A facility for non-fatal parser warnings
 * A convenient way to add specific warnings for invalid documentation
   comments
 * Warnings for module doc comments (which are not currently supported)
Fix parameter name propagation

If a name n appears in a parameter (which is therefore fixed) then n is
still fixed itself.
Merge pull request #917 from david-christiansen/bounded

Add type classes for bounded things
Merge pull request #918 from JanBessai/TotalNatOrder

Total order on Nat
Merge pull request #919 from hannesm/fix-rts-idris-net

Fix include for sockaddr_in and initialization of addr in idrnet_sockaddr_ipv4
Merge pull request #921 from david-christiansen/parse-doc-comment-warnings

Parser warnings; especially for invalid doc comments
Don't check hostname on network connections to REPL from editors.

It's already restricted to only listening on the 127.0.0.1 interface;
the additional check might just be being paranoid. Doesn't seem like
this kind of thing is a huge security concern, anyways.
Fixes #916.
Think I saw someone else complain about this too, recently.
Fix typo in usage message
Merge pull request #922 from LeifW/dont_check_hostname_in_repl

Don't check hostname on network connections to REPL from editors.
Merge pull request #923 from CodeBlock/patch-1

Fix typo in usage message
Prover commands for evaluation and typechecking expressions

Now, the prover supports two new commands:

 * :t, :type gives the type of an expression
 * :e, :eval normalises the expression and prints the result

These work within the proof environment, so evaluating expressions that
contain references to hypotheses is allowed.