mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-13 15:36:41 +03:00
Fix missing index contents
This commit is contained in:
parent
18931a41bf
commit
434dbabf7f
@ -105,6 +105,7 @@ Language Reference
|
||||
reference/packages
|
||||
reference/uniqueness-types
|
||||
reference/ffi
|
||||
reference/syntax-guide
|
||||
reference/erasure
|
||||
reference/ide-protocol
|
||||
reference/semantic-highlighting
|
||||
@ -113,6 +114,7 @@ Language Reference
|
||||
reference/compilation
|
||||
reference/language-features
|
||||
reference/language-extensions
|
||||
reference/elaborator-reflection
|
||||
reference/misc
|
||||
|
||||
.. _guides:
|
||||
|
@ -24,11 +24,12 @@ This will tell you how Idris works, for using it you should read the Idris Tutor
|
||||
packages
|
||||
uniqueness-types
|
||||
ffi
|
||||
erasure
|
||||
semantic-highlighting
|
||||
repl
|
||||
syntax-guide
|
||||
erasure
|
||||
ide-protocol
|
||||
semantic-highlighting
|
||||
tactics
|
||||
repl
|
||||
compilation
|
||||
language-features
|
||||
language-extensions
|
||||
|
Loading…
Reference in New Issue
Block a user