bend-ml-nat-lemmas
Releases (3)
Definitions (19)
main.bend
- def productProduct of the elements of a list of Nat; the empty list is 1.
- law add_zero
- law add_succ
- law add_comm
- law add_assoc
- law mul_zero
- def add_swapx + (y + z) == y + (x + z): swaps the middle terms of a triple sum.
- law mul_succ
- law mul_comm
- law mul_dist
- law mul_assoc
- law add4
- law mul_dist_l
- law mul_one_l
- law mul_one_r
- law append_nil
- law append_assoc
- law length_append
- law product_append