LAWS.bend source

LAWS.bend on the hub · documented module

# LAWS.bend -- the spec. A human writes this; the AI never touches it.# Each `law` is an open claim until PROOF.bend closes it.import Baseimport ./src/math.bend as M# for every x, x + 0 == xlaw add_zero:  for x: Nat  {Nat.add(x, 0n) == x : Nat}# appending the empty list on the right changes nothinglaw append_nil:  for xs: List<Nat>  {List.append(&1, Nat, xs, Nil{}) == xs : List<Nat>}# about *our* code: total distributes over a conslaw total_cons:  for h: Nat  for t: List<Nat>  {M.total(h <> t) == Nat.add(h, M.total(t)) : Nat}