Markdown indented code blocks (#20473)
* Implement Markdown indented code blocks
Additional indentation of 4 spaces makes a block an "indented code block"
(monospaced text without syntax highlighting).
Also `::` RST syntax for code blocks is disabled.
So instead of
```rst
see::
Some code
```
the code block should be written as
```markdown
see:
Some code
```
* Migrate RST literal blocks :: to Markdown's ones
This commit is contained in:
parent
594e93a66b
commit
6505bd347d
33 changed files with 697 additions and 603 deletions
36
doc/drnim.md
36
doc/drnim.md
|
|
@ -66,9 +66,9 @@ without additional annotations:
|
|||
```
|
||||
|
||||
This program contains a famous "index out of bounds" bug. DrNim
|
||||
detects it and produces the following error message::
|
||||
detects it and produces the following error message:
|
||||
|
||||
cannot prove: i <= len(a) + -1; counter example: i -> 0 a.len -> 0 [IndexCheck]
|
||||
cannot prove: i <= len(a) + -1; counter example: i -> 0 a.len -> 0 [IndexCheck]
|
||||
|
||||
In other words for `i == 0` and `a.len == 0` (for example!) there would be
|
||||
an index out of bounds error.
|
||||
|
|
@ -146,9 +146,9 @@ Example: insertionSort
|
|||
Unfortunately, the invariants required to prove that this code is correct take more
|
||||
code than the imperative instructions. However, this effort can be compensated
|
||||
by the fact that the result needs very little testing. Be aware though that
|
||||
DrNim only proves that after `insertionSort` this condition holds::
|
||||
DrNim only proves that after `insertionSort` this condition holds:
|
||||
|
||||
forall(i in 1..<a.len, a[i-1] <= a[i])
|
||||
forall(i in 1..<a.len, a[i-1] <= a[i])
|
||||
|
||||
|
||||
This is required, but not sufficient to describe that a `sort` operation
|
||||
|
|
@ -170,23 +170,23 @@ Syntax of propositions
|
|||
======================
|
||||
|
||||
The basic syntax is `ensures|requires|invariant: <prop>`.
|
||||
A `prop` is either a comparison or a compound::
|
||||
A `prop` is either a comparison or a compound:
|
||||
|
||||
prop = nim_bool_expression
|
||||
| prop 'and' prop
|
||||
| prop 'or' prop
|
||||
| prop '->' prop # implication
|
||||
| prop '<->' prop
|
||||
| 'not' prop
|
||||
| '(' prop ')' # you can group props via ()
|
||||
| forallProp
|
||||
| existsProp
|
||||
prop = nim_bool_expression
|
||||
| prop 'and' prop
|
||||
| prop 'or' prop
|
||||
| prop '->' prop # implication
|
||||
| prop '<->' prop
|
||||
| 'not' prop
|
||||
| '(' prop ')' # you can group props via ()
|
||||
| forallProp
|
||||
| existsProp
|
||||
|
||||
forallProp = 'forall' '(' quantifierList ',' prop ')'
|
||||
existsProp = 'exists' '(' quantifierList ',' prop ')'
|
||||
forallProp = 'forall' '(' quantifierList ',' prop ')'
|
||||
existsProp = 'exists' '(' quantifierList ',' prop ')'
|
||||
|
||||
quantifierList = quantifier (',' quantifier)*
|
||||
quantifier = <new identifier> 'in' nim_iteration_expression
|
||||
quantifierList = quantifier (',' quantifier)*
|
||||
quantifier = <new identifier> 'in' nim_iteration_expression
|
||||
|
||||
|
||||
`nim_iteration_expression` here is an ordinary expression of Nim code
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue