@@ -11,18 +11,21 @@ Compilation Process
12Idris follows the following compilation process:
12Idris follows the following compilation process:
14−1. Parsing
14+#. Parsing
15−2. Type Checking
15+#. Type Checking
16− 1. Elaboration
17+ #. Elaboration
17− 2. Coverage
18+ #. Coverage
18− 2. Unification
19+ #. Unification
19− 1. Totality Checking
20+ #. Totality Checking
20− 1. Erasure
21+ #. Erasure
21−3. Code Generation
23+#. Code Generation
22− 1. Defunctionalisation
25+ #. Defunctionalisation
23− 1. Inlining
26+ #. Inlining
24− 1. Resolving variables
27+ #. Resolving variables
25− 2. Code Generation
28+ #. Code Generation
28Type Checking Only
31Type Checking Only
@@ -31,8 +34,10 @@ Type Checking Only
31With Idris you can ask it to terminate the compilation process after type checking has completed. This is achieved through use of either:
34With Idris you can ask it to terminate the compilation process after type checking has completed. This is achieved through use of either:
33+ The command line options
36+ The command line options
34 + ``--check`` for files
38 + ``--check`` for files
35 + ``--checkpkg`` for packages
39 + ``--checkpkg`` for packages
36+ The REPL command: ``:check``
41+ The REPL command: ``:check``
38Use 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.
43Use 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.