vyrn
Menu
SourceCopy page
▾
Copy pageMarkdown, ready to paste into an LLMView as MarkdownThis page as plain textOpen in ClaudeAsk Claude about this page

std/proof

1 export, from std/proof.vyrn.

Comparisons the compiler proves where a call states them. prove is compiler-known: the compiler reads it by this declaration. Asks the compiler to prove c where the call stands. c is one integer comparison or several joined by &&. A c the prover cannot show is a refusal that names the comparison and why, and after the call every later check may assume c. The call checks nothing at run time.

Dependencies

The import graph shows the whole library.

Imports
nothing else in std/
Imported by
no other std module

prove fn

std/proof.vyrn, line 8
fn prove(c: Bool)

Asks the compiler to prove c where the call stands. c is one integer comparison or several joined by &&. A c the prover cannot show is a refusal that names the comparison and why, and after the call every later check may assume c. The call checks nothing at run time.

Tests

Test names

    This module carries no test block of its own.

    Examples

    1 program in examples/ import this module. Each runs as WebAssembly and as a native binary.