~/bend-docscommunity

nat.bend checks

raw source on the hub · import 0xfa577b9cd7c0487dc8d5d772f4bba913/nat.bend as MNat

1 import
import Base

Definitions

def add_zero source · line 13 · raw

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

def add_assoc source · line 21 · raw

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