Health.Health.heal_agrees: law of gralha-bendquest@0.1.0.0
Import: import gralha-bendquest@0.1.0.0/health.bend as Health
Lines 263-267 of gralha-bendquest@0.1.0.0/health.bend: https://jend.leeeet.dev/read.txt?path=gralha-bendquest@0.1.0.0/health.bend&start_line=263&end_line=267

import Base

law Health.heal_agrees:
  for +hp: Nat
  for +amount: Nat
  for +maximum: Nat
  {Health.heal(hp, amount, maximum) == Health.spec_heal(hp, amount, maximum) : Nat}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/health.bend&name=Health.add_agrees
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/health.bend&name=Health.clamp_agrees
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/health.bend&name=Health.heal
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/health.bend&name=Health.spec_clamp
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/health.bend&name=Health.spec_heal