idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-14 22:02:07 +03:00
Code Issues Projects Releases Wiki Activity

[ doc ] add missing backquote

Browse Source
This commit is contained in:
Sage Hane 2022-03-07 21:12:36 +09:00 committed by G. Allais
parent 1c396744d9
commit c2718684d8
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Idris/Doc/Keywords.idr
View File

@ -93,7 +93,7 @@ totality = vcat $
header "Totality" :: "" header "Totality" :: ""
:: map (indent 2) [ :: map (indent 2) [
""" """
Definitions can be individually declared `total`, `covering`, or partial`. Definitions can be individually declared `total`, `covering`, or `partial`.
It is also possible to set the default totality flag for definitions in a It is also possible to set the default totality flag for definitions in a
module by using the `%default` pragma. module by using the `%default` pragma.
""", "", """, "",