law Growth.level_up_preserves_health
gralha-bendquest@0.1.0.0 · growth.bend:155
import gralha-bendquest@0.1.0.0/growth.bend as Growth
import Base
import gralha-bendquest@0.1.0.0/game.bend as G
155law Growth.level_up_preserves_health:
156 for +hp: U32
157 for +level: Nat
158 for +vitality: Nat
159 for +bonus: U32
160 for +ceiling: U32
161 for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Growth.maximum(level, vitality, bonus, ceiling))) == True{} : Bool}
162 {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Growth.maximum(Succ{level}, vitality, bonus, ceiling))) == True{} : Bool}