Rzk proof assistant
Directed interval
English
Русский
Initializing search
rzk-lang/rzk
About
Getting Started
Reference
Playground
Blog
Rzk proof assistant
rzk-lang/rzk
About
Getting Started
Reference
Reference
Introduction
Cube layer
Tope layer
Dependent types
Tope disjunction elimination
Extension types
Organizational features
Organizational features
Sections and Variables
Builtins
Builtins
Directed interval
Unit type
Commands
Commands
Define and Postulate
Compute
Check
Options
Other
Other
Rendering Diagrams
Examples
Examples
Weak tope disjunction elimination
Playground
Blog
Directed interval