~/bend-docscommunity

add_zero.bend checks

raw source on the hub · import 0x6ab8d4bb6183370cf3b7d5d7fda20aff/add_zero.bend as Add_zero

Adding zero changes nothing: one proof, published to test the hub

1 import
import Base

Laws

law add_zero proved

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 4 · raw

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