~/bend-docscommunity

mul.bend checks

raw source on the hub · import 0xb13667d52aa56e002b4d09883d7fce3e/mul.bend as Mul

mul.bend: laws of Base's Nat.mul. Kept apart from nat.bend because the proofs use ac.bend, which imports nat.bend.

3 imports
import Base
import ./nat.bend as N
import ./ac.bend as A

Definitions

def mul_add_r_rev source · line 8 · raw

@+a:Nat -> @+b:Nat -> @+x:Nat -> {Nat.add(Nat.mul(a, x), Nat.mul(b, x)) == Nat.mul(Nat.add(a, b), x) : Nat}

def mul_add_l source · line 11 · raw

@+x:Nat -> @+y:Nat -> @+z:Nat -> {Nat.mul(x, Nat.add(y, z)) == Nat.add(Nat.mul(x, y), Nat.mul(x, z)) : Nat}

def mul_assoc source · line 21 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(Nat.mul(a, b), c) : Nat}

def mul_double_l source · line 30 · raw

@+x:Nat -> @+y:Nat -> {Nat.double(Nat.mul(x, y)) == Nat.mul(Nat.double(x), y) : Nat}

def mul_double_r source · line 40 · raw

@+x:Nat -> @+y:Nat -> {Nat.double(Nat.mul(x, y)) == Nat.mul(x, Nat.double(y)) : Nat}

def mul_zero source · line 50 · raw

@+a:Nat -> {Nat.mul(a, 0n) == 0n : Nat}

def mul_succ source · line 57 · raw

@+a:Nat -> @+b:Nat -> {Nat.add(a, Nat.mul(a, b)) == Nat.mul(a, 1n+b) : Nat}

def mul_comm source · line 66 · raw

@+a:Nat -> @+b:Nat -> {Nat.mul(a, b) == Nat.mul(b, a) : Nat}