def Health.clamp_word

gralha-bendquest@0.1.0.0 · health.bend:315

import gralha-bendquest@0.1.0.0/health.bend as Health

import Base

315# Existing U32 records enter the rules here. The refinement and preservation
316# theorems below prove these exact word wrappers cannot wrap their results.
317def Health.clamp_word(hp: U32, maximum: U32) -> U32:
318  U32.from_nat(Health.clamp(U32.to_nat(hp), U32.to_nat(maximum)))

Uses (4)

Used by (2)