mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
docs: Fix indentation in some of the code snippets
This commit is contained in:
parent
ce79e2515b
commit
42f982c063
@ -52,6 +52,7 @@ where the default is no engine. Selecting the engine enables the SMTChecker on a
|
|||||||
enables the SMTChecker for all files.
|
enables the SMTChecker for all files.
|
||||||
|
|
||||||
.. note::
|
.. note::
|
||||||
|
|
||||||
The lack of warnings for a verification target represents an undisputed
|
The lack of warnings for a verification target represents an undisputed
|
||||||
mathematical proof of correctness, assuming no bugs in the SMTChecker and
|
mathematical proof of correctness, assuming no bugs in the SMTChecker and
|
||||||
the underlying solver. Keep in mind that these problems are
|
the underlying solver. Keep in mind that these problems are
|
||||||
@ -202,6 +203,7 @@ Note that in this example the SMTChecker will automatically try to prove three p
|
|||||||
3. The assertion is always true.
|
3. The assertion is always true.
|
||||||
|
|
||||||
.. note::
|
.. note::
|
||||||
|
|
||||||
The properties involve loops, which makes it *much much* harder than the previous
|
The properties involve loops, which makes it *much much* harder than the previous
|
||||||
examples, so beware of loops!
|
examples, so beware of loops!
|
||||||
|
|
||||||
@ -500,7 +502,6 @@ which has the following form:
|
|||||||
"source2.sol": ["contract2", "contract3"]
|
"source2.sol": ["contract2", "contract3"]
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
.. _smtchecker_engines:
|
.. _smtchecker_engines:
|
||||||
|
|
||||||
Natspec Function Abstraction
|
Natspec Function Abstraction
|
||||||
|
Loading…
Reference in New Issue
Block a user