law Health.spec_clamp_unchanged

gralha-bendquest@0.1.0.0 · health.bend:58

import Base
import gralha-bendquest@0.1.0.0/game.bend as G

58law Health.spec_clamp_unchanged:
59  for +hp: Nat
60  for +maximum: Nat
61  for +valid: {G.Bq.Nat.le(hp, maximum) == True{} : Bool}
62  {Health.spec_clamp(hp, maximum) == hp : Nat}