law Growth.vitality_up_preserves_health

gralha-bendquest@0.1.0.0 · growth.bend:167

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

167law Growth.vitality_up_preserves_health:
168  for +hp: U32
169  for +level: Nat
170  for +vitality: Nat
171  for +bonus: U32
172  for +ceiling: U32
173  for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Growth.maximum(level, vitality, bonus, ceiling))) == True{} : Bool}
174  {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Growth.maximum(level, Succ{vitality}, bonus, ceiling))) == True{} : Bool}