Eutaxy

eutaxy/spec ​

import { … } from "eutaxy/spec"; 3 functions and values, 4 types; each links to the file that declares it.

Functions, classes and values ​

forall ​

function forall<F extends Fn>(fn: F, property: { readonly sample?: (...args: Parameters<F>) => boolean; readonly when?: (...args: Parameters<F>) => boolean; readonly ensures: (...args: Parameters<F>) => boolean; }): Forall<F>

Claim that ensures holds for every input of fn where when holds; sample narrows only the inputs the TESTED rung draws. Source

isSpec ​

function isSpec(value: unknown): value is Spec

Whether a spec file's export is one of the two spec shapes. Source

total ​

function total<F extends Fn>(fn: F): Total<F>

Claim that fn terminates on every input of its parameter types; only an engine can establish it. Source

Types ​

Fn ​

type Fn

Any function; never[] so that every parameter list is accepted. Source

Forall ​

interface Forall

A universally quantified claim: for every input of fn's parameter types where when holds, ensures holds. Source

Spec ​

type Spec

A spec file's export: a forall claim or a total claim. Source

Total ​

interface Total

The claim that fn terminates on every input of its parameter types. Source