~/bend-docscommunity

LAWS.bend open laws/TODOs

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

LAWS.bend -- the spec. A human writes this; the AI never touches it. Each law is an open claim until PROOF.bend closes it.

2 imports
import Base
import ./src/math.bend as M

Laws

law add_zero provedin PROOF.bend

Also proved in bend-mathlib as nat.add_zero: import bend-mathlib@0.7.2.0/nat.bend as MNat, then MNat.add_zero.

source · line 8 · raw

@x:Nat -> {Nat.add(x, 0n) == x : Nat}

for every x, x + 0 == x

law append_nil provedin PROOF.bendsource · line 13 · raw

@xs:List<&1, Nat> -> {List.append(&1, Nat, xs, []) == xs : List<&1, Nat>}

appending the empty list on the right changes nothing

law total_cons provedin PROOF.bendsource · line 18 · raw

@h:Nat -> @t:List<&1, Nat> -> {0x983079cc7642e53dbc9aaf7fa2636b20/src/math.total(h <> t) == Nat.add(h, 0x983079cc7642e53dbc9aaf7fa2636b20/src/math.total(t)) : Nat}

about *our* code: total distributes over a cons