From 8de3aa7a017c97df2e9cbd21a7e315a6dcd69dba Mon Sep 17 00:00:00 2001 From: Jan de Muijnck-Hughes Date: Sun, 31 May 2015 22:05:47 +0100 Subject: [PATCH] Fixed indentation of enumerated list. --- docs/reference/compilation.rst | 29 +++++++++++++++++------------ 1 file changed, 17 insertions(+), 12 deletions(-) diff --git a/docs/reference/compilation.rst b/docs/reference/compilation.rst index 429a44db8..41a87f450 100644 --- a/docs/reference/compilation.rst +++ b/docs/reference/compilation.rst @@ -11,18 +11,21 @@ Compilation Process Idris follows the following compilation process: -1. Parsing -2. Type Checking - 1. Elaboration - 2. Coverage - 2. Unification - 1. Totality Checking - 1. Erasure -3. Code Generation - 1. Defunctionalisation - 1. Inlining - 1. Resolving variables - 2. Code Generation +#. Parsing +#. Type Checking + + #. Elaboration + #. Coverage + #. Unification + #. Totality Checking + #. Erasure + +#. Code Generation + + #. Defunctionalisation + #. Inlining + #. Resolving variables + #. Code Generation Type Checking Only @@ -31,8 +34,10 @@ Type Checking Only With Idris you can ask it to terminate the compilation process after type checking has completed. This is achieved through use of either: + The command line options + + ``--check`` for files + ``--checkpkg`` for packages + + The REPL command: ``:check`` Use of this option will still result in the generation of the Idris binary ``.ibc`` files, and is suitable if you do not wish to generate code from one of the supported backends.