~/bend-docscommunity

LAWS.bend open laws/TODOs

raw source on the hub · import 0x7e29b7224f420229b0320d908dff8769/LAWS.bend as LAWS

3 imports
import Base
import ./src/batch.bend as Batch
import ./src/linear_regression.bend as Linear

Laws

law prediction_count provedin PROOF.bendsource · line 6 · raw

@+model:0x7e29b7224f420229b0320d908dff8769/src/linear_regression.Model -> @+rows:0x7e29b7224f420229b0320d908dff8769/src/batch.Batch<F32> -> {0x7e29b7224f420229b0320d908dff8769/src/batch.count(F32, 0x7e29b7224f420229b0320d908dff8769/src/linear_regression.predict_batch(model, rows)) == 0x7e29b7224f420229b0320d908dff8769/src/batch.count(F32, rows) : Nat}

Structural guarantees only: these make no claims about F32 accuracy.

law rejects_empty_training provedin PROOF.bendsource · line 11 · raw

{0x7e29b7224f420229b0320d908dff8769/src/linear_regression.fit(0x7e29b7224f420229b0320d908dff8769/src/batch.Empty{}) == Fail{0x7e29b7224f420229b0320d908dff8769/src/linear_regression.NotEnoughSamples{}} : Result<&2, &2, 0x7e29b7224f420229b0320d908dff8769/src/linear_regression.FitError, 0x7e29b7224f420229b0320d908dff8769/src/linear_regression.Model>}