Introduction
1.
Installation
1.1.
opam package manager
1.2.
Install Coq
1.3.
Install Pruvendo libraries
1.4.
Install via Docker image
2.
Quick start
2.1.
Write simple contract
2.2.
Compile and extract solidity sources
2.3.
Compile extracted contract and deploy
3.
Coq embedded DSL
3.1.
Coq custom grammar
3.2.
Ursus embedding
3.3.
Notational mechanism
4.
Ursus as a language
4.1.
Interface structure
4.2.
Contract structure
4.3.
Types, primitives, and literals
4.4.
Complex Structures
4.5.
How to write Ursus functions
4.6.
Interfaces and messages
4.7.
Local state and variables
4.8.
Multi-contract system
4.9.
Contract inheritance
5.
Ursus standard library
5.1.
Standard functions
5.2.
Basic operators
5.3.
TVM functions
6.
Ursus verification
6.1.
Common principles
6.2.
StdLib verification
6.3.
QuickChick
7.
Ursus programming style
7.1.
REPL
7.2.
Goal and context
7.3.
Tactics and tacticals
7.3.1.
Ursus control sub-languange
7.4.
Holes
7.5.
Default prefix and postfix operations
8.
Long start
8.1.
Designing contract
8.2.
Implementation
8.3.
Extracting, compiling and deploy
8.4.
Specification
8.5.
TS4 integration
8.6.
Quickchicks
8.7.
Evals and execs
8.8.
Direct proofs
8.9.
Scenarios
8.10.
Multi-contract verification
9.
Translation
9.1.
sol->ursus translation
9.2.
cpp->ursus translation
9.3.
ursus->sol translation
10.
Advanced topics
10.1.
Ledger and Superledger
10.2.
Specification
10.3.
Proof kinds
10.4.
Evals and execs generator
10.5.
Elpi automation
11.
More and uncategorized
Light (default)
Rust
Coal
Navy
Ayu
Ursus language documentation
Compiling and deplying Solidity
TODO