~/jendhub

def mul_zero_right

bendtorch-core@0.1.0.0 · src/shape/nat_proofs.bend:61

import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as NatProofs
import Base

61def mul_zero_right(+a: Nat) -> {Nat.mul(a, 0n) == 0n : Nat}:
62  match a:
63    case 0n:
64      {==}
65    case 1n+p:
66      mul_zero_right(p)

Uses (2)

Used by (6)