mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-28 02:23:44 +03:00
Merge pull request #2878 from nukisman/patch-2
Fix typo in custom backend cookbook
This commit is contained in:
commit
238de10a35
@ -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)
|
Now lets turn our attention to the different intermediate representations (IRs)
|
||||||
that Idris provides.
|
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
|
it will produce a ``CompileData`` record, which will contain lists of top-level
|
||||||
definitions that needs to be compiled. These are:
|
definitions that needs to be compiled. These are:
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user