~/jendhub

law Bq.buy_burns_exact_gold

gralha-bendquest@0.1.0.0 · game.bend:950

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

950law Bq.buy_burns_exact_gold:
951  (@+k_0: Nat -> (@+h_1: Bq.Hero -> (@+__2: {Bq.buy_ok(k_0, h_1) == True{} : Bool} -> {Bq.Nat.add(Bq.iprice(k_0), Bq.hero_gold(Bq.hero_step(Bq.HOp.Buy{k_0}, h_1))) == Bq.hero_gold(h_1) : Nat})))

Uses (17)

Used by (0)

No other definition uses this definition.