10 lines
465 B
Text
10 lines
465 B
Text
|
(according to Gemini AI):
|
||
|
|
|
||
|
|
Idris2 uses comment characters similar to Haskell:
|
||
|
|
|
||
|
|
Single-line comments: Start with -- (two hyphens). Everything from -- to the end of the line is a comment.
|
||
|
|
|
||
|
|
Multi-line comments: Enclosed by {- and -}. These can span multiple lines and can also be nested.
|
||
|
|
|
||
|
|
Additionally, Idris2 supports inline documentation comments which begin with ||| (three pipe symbols). These are parsed by the compiler and can be used to generate documentation.
|