def minz

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64mulp.bend:35

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulp.bend as F64mulp

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL

35def minz(+r: Nat) -> {Nat.min(r, 0n) == 0n : Nat}:
36  FL.minz(r)

Uses (3)

Nat
Nat.min
bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light:minz

Used by (0)

No other definition uses this definition.