source/docs/guide/src · verus · Tangled

forked from verus-lang/verus

verus source docs guide src

1 folder · 159 files

Bryan Parno · Swap from will_return_none to produces (#3330) · 2w ago

guide: add styling for a 'Verus/Rust difference' note (#2602)

assert_assume.md

Guide typos (#3340)

assert_by_compute.md

Guide typos (#3340)

Minor docs formatting changes

assert-mut-ref.md

guide: clean up the new ownership and borrowing section

binary_search.md

Guide typos (#3340)

Guide typos (#3340)

Rename examples directory (rename source/rust_verify/example to examples)

breaking_proofs_into_pieces.md

Guide typos (#3340)

broadcast_proof.md

Guide typos (#3340)

Guide typos (#3340)

call-from-unverified-code.md

Guide typos (#3340)

calling-unverified-from-verified.md

Guide typos (#3340)

calling-verified-from-unverified.md

Guide typos (#3340)

Guide typos (#3340)

guide: add proof debugging checklist

complex_ownership.md

guide: organize the Rust unsafe/concurrency chapters

Guide typos (#3340)

Guide typos (#3340)

container_bst_all_source.md

Rename examples directory (rename source/rust_verify/example to examples)

container_bst_clone.md

Guide typos (#3340)

container_bst_first_draft.md

Guide typos (#3340)

container_bst_generic.md

Guide typos (#3340)

container_bst_mut_refs.md

Guide typos (#3340)

container_bst_type_invariant.md

Guide typos (#3340)

container_bst.md

Minor edits to the new BST example

Add documentation for exec_spec, dual_spec, and attribute-based syntax (#1910)

datatypes_enum.md

Guide typos (#3340)

datatypes_struct.md

Rename examples directory (rename source/rust_verify/example to examples)

add struct, enum section to guide (#1193)

develop_proofs.md

New documentation page on devising invariants (#1381)

Guide typos (#3340)

Guide typos (#3340)

Guide typos (#3340)

exec_closures.md

Guide typos (#3340)

exec_funs_as_values.md

Guide typos (#3340)

Guide typos (#3340)

Guide typos (#3340)

exec_termination.md

Guide typos (#3340)

exec_to_spec.md

Guide typos (#3340)

Guide typos (#3340)

extensional_equality.md

Guide typos (#3340)

external_trait_specifications.md

Guide typos (#3340)

Guide typos (#3340)

Guide typos (#3340)

Guide typos (#3340)

getting_started_cmd_line.md

Guide typos (#3340)

getting_started_vscode.md

Guide typos (#3340)

getting_started.md

Guide typos (#3340)

ghost_vs_exec.md

Guide typos (#3340)

Guide typos (#3340)

higher-order-fns.md

Guide typos (#3340)

Guide typos (#3340)

Guide typos (#3340)

install-singular.md

[vargo] feat: deprecate Vargo (#3105)

Guide typos (#3340)

interacting-with-unverified-code.md

Guide typos (#3340)

interior_mutability.md

Guide typos (#3340)

Guide typos (#3340)

iterator-specs-finite.md

Swap from will_return_none to produces (#3330)

iterator-specs-infinite.md

Swap from will_return_none to produces (#3330)

iterator-specs.md

Update iterator documentation in the Guide (#2747)

Guide typos (#3340)

Guide typos (#3340)

llmforverusproof.md

Guide typos (#3340)

Adding a LLMs-for-Verus chapter into the tutorial. (#2429)

logatom-call.md

Guide typos (#3340)

logatom-open.md

Guide typos (#3340)

logatom-spec.md

Guide typos (#3340)

Guide typos (#3340)

memory-safety.md

Guide typos (#3340)

Rename examples directory (rename source/rust_verify/example to examples)

multitriggers.md

Guide typos (#3340)

mutable-references.md

Guide typos (#3340)

mutation-references-borrowing.md

Guide typos (#3340)

Guide typos (#3340)

Guide typos (#3340)

Guide typos (#3340)

Rename examples directory (rename source/rust_verify/example to examples)

Guide typos (#3340)

Guide typos (#3340)

Guide typos (#3340)

guide: organize the Rust unsafe/concurrency chapters

prefix-and-or.md

Flesh out the reference section for spec expressions (#2467)

Guide typos (#3340)

Add documentation about `cargo verus` (#2535)

proof_functions.md

Rename examples directory (rename source/rust_verify/example to examples)

Rename examples directory (rename source/rust_verify/example to examples)

Rename examples directory (rename source/rust_verify/example to examples)

recursion_loops.md

Guide typos (#3340)

Guide typos (#3340)

ref-extensional-equality.md

Check doc crosslinks in CI and fix broken links (#3141)

reference-as.md

Check doc crosslinks in CI and fix broken links (#3141)

reference-assert-by-prover.md

Guide typos (#3340)

reference-assert-by.md

Flesh out the reference section for spec expressions (#2467)

reference-assert-forall-by.md

Flesh out the reference section for spec expressions (#2467)

reference-assert.md

Guide typos (#3340)

reference-assume-specification.md

Guide typos (#3340)

reference-assume.md

Organize reference pages for prover modes (#2613)

reference-at-sign.md

Guide typos (#3340)

reference-attributes.md

Guide typos (#3340)

reference-chained-op.md

Flesh out the reference section for spec expressions (#2467)

reference-decreases-to.md

Guide typos (#3340)

reference-decreases.md

Guide typos (#3340)

reference-exec-signature.md

Guide typos (#3340)

reference-flag-record.md

Error report (#612)

reference-global.md

Guide typos (#3340)

reference-has.md

Guide typos (#3340)

reference-implication.md

Guide typos (#3340)

reference-is.md

Flesh out the reference section for spec expressions (#2467)

reference-matches.md

Flesh out the reference section for spec expressions (#2467)

reference-opens-invariants.md

guide: update opens_invariants docs

reference-pointers-cells.md

Flesh out new raw_ptr interface (#1244)

reference-proof-signature.md

Guide typos (#3340)

reference-prover-mode-bit-vector.md

Guide typos (#3340)

reference-prover-mode-compute.md

Guide typos (#3340)

reference-prover-mode-integer-ring.md

Guide typos (#3340)

reference-prover-mode-nonlinear.md

Guide typos (#3340)

reference-recommends.md

guide: add reference page on `returns` clause, function signatures

reference-returns.md

Guide typos (#3340)

reference-reveal-hide.md

Guide typos (#3340)

reference-reveal-strlit.md

Flesh out the reference section for spec expressions (#2467)

reference-signature-fnonce.md

add reference material on trait signatures and FnOnce

reference-signature-inheritance.md

reference-spec-index.md

Guide typos (#3340)

reference-spec-signature.md

Guide typos (#3340)

reference-specification-language.md

Guide typos (#3340)

reference-type-invariants.md

Guide typos (#3340)

reference-types.md

Guide typos (#3340)

reference-unions.md

Flesh out the reference section for spec expressions (#2467)

reference-unwind-sig.md

Guide typos (#3340)

reference-var-modes.md

Guide typos (#3340)

requires_ensures.md

Guide typos (#3340)

smt_failures.md

Guide typos (#3340)

smt_perf_overview.md

Expand documentation on performance measurement. Also cleanup the ToC a bit. (#1215)

spec_closures.md

Rename examples directory (rename source/rust_verify/example to examples)

spec_functions.md

Guide typos (#3340)

Guide typos (#3340)

spec_vs_proof.md

Guide typos (#3340)

spec-arithmetic.md

Guide typos (#3340)

spec-bit-ops.md

Guide typos (#3340)

Flesh out the reference section for spec expressions (#2467)

spec-equality.md

Organize reference pages for prover modes (#2613)

spec-expressions.md

Flesh out the reference section for spec expressions (#2467)

spec-operator-precedence.md

Flesh out the reference section for spec expressions (#2467)

spec-quantifiers.md

Flesh out the reference section for spec expressions (#2467)

spec-rust-subset.md

Guide typos (#3340)

Add more to docs/guide

update supported features list, add docs for static items

Guide typos (#3340)

Guide typos (#3340)

Guide typos (#3340)

Guide typos (#3340)

Add documentation for traits (#2537)

Guide typos (#3340)

trigger-annotations.md

Guide typos (#3340)

verus_macro_intro.md

guide: update supported features table (#2443)

Guide typos (#3340)

Add a brief intro to the Libraries section of of the documentation, mentionining `vstd` and `vstd::prelude`

Rename examples directory (rename source/rust_verify/example to examples)