Introduction
1.
Build System
1.1.
Project Structure
1.2.
Manifest File Format
1.3.
Module System
1.4.
Dependency Resolution Strategy
2.
Syntax and Semantics
2.1.
Comments
2.1.1.
Line
2.1.2.
Block
2.2.
Identifiers
2.3.
Paths
2.4.
Flow Control Structures
2.4.1.
Block
2.5.
Types
2.5.1.
Primitive
2.5.1.1.
nothing
2.5.1.2.
bool
2.5.1.3.
u8
2.5.1.4.
u16
2.5.1.5.
u32
2.5.1.6.
u64
2.5.1.7.
usize
2.5.1.8.
i8
2.5.1.9.
i16
2.5.1.10.
i32
2.5.1.11.
i64
2.5.1.12.
isize
2.6.
Expressions
2.6.1.
Literal
2.6.1.1.
Boolean
2.6.1.2.
Integer
2.6.2.
Item
2.6.3.
Call
2.6.4.
Syscall
2.6.5.
Block
2.7.
Specifications
2.7.1.
Propositions
2.7.2.
Assumes
2.7.3.
Requires
2.7.4.
Ensures
2.8.
Statements
2.8.1.
Import
2.8.2.
Export
2.8.3.
Function Definition
2.8.4.
Expression
2.8.5.
Block
2.9.
Complete Grammar
2.10.
Name Resolution
2.11.
Type Checking
2.12.
Type Inference
Light (default)
Rust
Coal
Navy
Ayu
The Protocol Verification Language Reference
Dependency Resolution Strategy
Coming soon...