@@ -11,18 +11,21 @@ Compilation Process
1111
1212Idris follows the following compilation process:
1313
14−1. Parsing
15−2. Type Checking
16− 1. Elaboration
17− 2. Coverage
18− 2. Unification
19− 1. Totality Checking
20− 1. Erasure
21−3. Code Generation
22− 1. Defunctionalisation
23− 1. Inlining
24− 1. Resolving variables
25− 2. Code Generation
14+#. Parsing
15+#. Type Checking
16+
17+ #. Elaboration
18+ #. Coverage
19+ #. Unification
20+ #. Totality Checking
21+ #. Erasure
22+
23+#. Code Generation
24+
25+ #. Defunctionalisation
26+ #. Inlining
27+ #. Resolving variables
28+ #. Code Generation
2629
2730
2831Type Checking Only
@@ -31,8 +34,10 @@ Type Checking Only
3134With Idris you can ask it to terminate the compilation process after type checking has completed. This is achieved through use of either:
3235
3336+ The command line options
37+
3438 + ``--check`` for files
3539 + ``--checkpkg`` for packages
40+
3641+ The REPL command: ``:check``
3742
3843Use 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.