Skip to content
CN Docs
Expressions
Initializing search
Getting started
Specifications
Reference
CN Docs
Getting started
Getting started
Installation
Tutorials
Tutorials
Basic usage
Pointers and simple ownership
Ownership of compound objects
Arrays and loops
Defining predicates
Allocating and deallocating memory
Lists
Working with external lemmas
Case studies
Case studies
Imperative queues
Doubly-linked lists
Airport Simulation
Style guide
Style guide
Specifications
Specifications
Function specifications
Loop invariants
Conditions
Expressions
Resource predicates
Auxiliary definitions
Auxiliary definitions
Data structures
Logical functions
Custom resource predicates
Types
Scoping
Tactics (proof hints)
Interactive theorem proving
Reference
Reference
Expressions
¶
Built-in data structures
¶
Back to top