mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-24 06:52:19 +03:00
Fix typo
This commit is contained in:
parent
464797944a
commit
09f97d673c
@ -120,7 +120,7 @@ Which Intermediate Representation (IR) should be consumed by the custom back-end
|
||||
|
||||
Now lets turn our attention to the different intermediate representations (IRs)
|
||||
that Idris provides.
|
||||
When the ``getCompiledData`` function is invoked with the ``Phase`` parameter
|
||||
When the ``getCompileData`` function is invoked with the ``Phase`` parameter
|
||||
it will produce a ``CompileData`` record, which will contain lists of top-level
|
||||
definitions that needs to be compiled. These are:
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user