Idris2Doc : Text.Markdown.String

Text.Markdown.String

(source)

Definitions

blankLine : Lexer
Totality: total
Visibility: export
headingSym : Lexer
Totality: total
Visibility: export
horizontalRules : Lexer
  A horizontal rule.

The horizontal rule is reprenseted by three or more consecutive '*', '-', or
'_' characters.

The current implementation allows for the horizontal rule to be directly
following the above block, without a blank line, for example:

```markdown
Hello world!
---
```

However, ideally, there should be a blank line before:

```markdown
Hello

---
```

Space characters are tolerated after the horizontal rule.

Totality: total
Visibility: export
imageSym : Lexer
Totality: total
Visibility: export
italicsSym : Lexer
Totality: total
Visibility: export
boldSym : Lexer
Totality: total
Visibility: export
Totality: total
Visibility: export
htmlOpenTag : Lexer
  Note: we currently don't allow attributes
To do so, we might need to move this from the lexer into the parser

Totality: total
Visibility: export
htmlCloseTag : Lexer
Totality: total
Visibility: export
pre : Lexer
Totality: total
Visibility: export
codeFence : Lexer
Totality: total
Visibility: export
text : Lexer
Totality: total
Visibility: export