gralha-bendquest

Releases (1):
  0.1.0.0  0x6f51b0319916bc200dd5f3949f31668e  indexed  https://jend.leeeet.dev/files.txt?path=gralha-bendquest@0.1.0.0

Definitions (307, 1 to 100 shown):
  Game.Bq.Bag (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bag)
   law Bq.Bag:
     Data
  Game.Bq.Maybe (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Maybe)
   law Bq.Maybe:
     (@-A_0: Data -> Data)
  Game.Bq.Hero (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Hero)
   type Bq.Hero is Data:
     Bq.Hero.Hero{inv_0: Bq.Bag, wea_1: Bq.Maybe(Nat), arm_2: Bq.Maybe(Nat), hel_3: Bq.Maybe(Nat), chm_4: Bq.Maybe(Nat), gold_5: Nat, lv_6: Nat, str_7: Nat, agi_8: Nat, vit_9: Nat, pts_10: Nat}
  Game.Bq.hero_gold (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.hero_gold)
   law Bq.hero_gold:
     (@+h_0: Bq.Hero -> Nat)
  Game.Bq.one (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.one)
   law Bq.one:
     (@+k_0: Nat -> Bq.Bag)
  Game.Bq.ISlot (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.ISlot)
   type Bq.ISlot is Data:
     Bq.ISlot.SlotW{}
     Bq.ISlot.SlotA{}
     Bq.ISlot.SlotH{}
     Bq.ISlot.SlotC{}
     Bq.ISlot.SlotNone{}
  Game.Bq.Info (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Info)
   type Bq.Info is Data:
     Bq.Info.Info{slot_0: Bq.ISlot, lvreq_1: Nat, streq_2: Nat, agireq_3: Nat, vitreq_4: Nat, atk_5: Nat, df_6: Nat, price_7: Nat}
  Game.Bq.info_potion (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.info_potion)
   law Bq.info_potion:
     Bq.Info
  Game.Bq.info_weapon (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.info_weapon)
   law Bq.info_weapon:
     (@+k_0: Nat -> Bq.Info)
  Game.Bq.info_armor (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.info_armor)
   law Bq.info_armor:
     (@+k_0: Nat -> Bq.Info)
  Game.Bq.info_helm (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.info_helm)
   law Bq.info_helm:
     (@+k_0: Nat -> Bq.Info)
  Game.Bq.info_charm (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.info_charm)
   law Bq.info_charm:
     (@+k_0: Nat -> Bq.Info)
  Game.Bq.Nat.sub (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Nat.sub)
   law Bq.Nat.sub:
     (@+a_0: Nat -> (@+b_1: Nat -> Nat))
  Game.Bq.Nat.le (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Nat.le)
   law Bq.Nat.le:
     (@+a_0: Nat -> (@+b_1: Nat -> Bool))
  Game.Bq.item_info (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.item_info)
   law Bq.item_info:
     (@+k_0: Nat -> Bq.Info)
  Game.Bq.islot (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.islot)
   law Bq.islot:
     (@+k_0: Nat -> Bq.ISlot)
  Game.Bq.Bag.sub (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bag.sub)
   law Bq.Bag.sub:
     (@+a_0: Bq.Bag -> (@+b_1: Bq.Bag -> Bq.Bag))
  Game.Bq.Maybe.some (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Maybe.some)
   law Bq.Maybe.some:
     (@-A_0: Data -> (@+value_1: A_0 -> Bq.Maybe(A_0)))
  Game.Bq.do_equip (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.do_equip)
   law Bq.do_equip:
     (@+k_0: Nat -> (@+h_1: Bq.Hero -> Bq.Hero))
  Game.Bq.mb (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.mb)
   law Bq.mb:
     (@+m_0: Bq.Maybe(Nat) -> Bq.Bag)
  Game.Bq.Nat.add (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Nat.add)
   law Bq.Nat.add:
     (@+a_0: Nat -> (@+b_1: Nat -> Nat))
  Game.Bq.Bag.add (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bag.add)
   law Bq.Bag.add:
     (@+a_0: Bq.Bag -> (@+b_1: Bq.Bag -> Bq.Bag))
  Game.Bq.Maybe.none (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Maybe.none)
   law Bq.Maybe.none:
     (@-A_0: Data -> Bq.Maybe(A_0))
  Game.Bq.do_unequip (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.do_unequip)
   law Bq.do_unequip:
     (@+s_0: Bq.ISlot -> (@+h_1: Bq.Hero -> Bq.Hero))
  Game.Bq.iprice (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.iprice)
   law Bq.iprice:
     (@+k_0: Nat -> Nat)
  Game.Bq.do_buy (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.do_buy)
   law Bq.do_buy:
     (@+k_0: Nat -> (@+h_1: Bq.Hero -> Bq.Hero))
  Game.Bq.POTION (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.POTION)
   law Bq.POTION:
     Nat
  Game.Bq.do_quaff (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.do_quaff)
   law Bq.do_quaff:
     (@+h_0: Bq.Hero -> Bq.Hero)
  Game.Bq.do_alloc (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.do_alloc)
   law Bq.do_alloc:
     (@+s_0: Nat -> (@+h_1: Bq.Hero -> Bq.Hero))
  Game.Bq.do_levelup (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.do_levelup)
   law Bq.do_levelup:
     (@+h_0: Bq.Hero -> Bq.Hero)
  Game.Bq.HOp (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.HOp)
   type Bq.HOp is Data:
     Bq.HOp.Equip{k_0: Nat}
     Bq.HOp.Unequip{s_0: Bq.ISlot}
     Bq.HOp.Buy{k_0: Nat}
     Bq.HOp.Quaff{}
     Bq.HOp.Alloc{s_0: Nat}
     Bq.HOp.LevelUp{}
  Game.Bq.hop_do (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.hop_do)
   law Bq.hop_do:
     (@+op_0: Bq.HOp -> (@+h_1: Bq.Hero -> Bq.Hero))
  Game.Bq.hero_step_go (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.hero_step_go)
   law Bq.hero_step_go:
     (@+v_0: Bool -> (@+op_1: Bq.HOp -> (@+h_2: Bq.Hero -> Bq.Hero)))
  Game.Bq.slot_empty (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.slot_empty)
   law Bq.slot_empty:
     (@+m_0: Bq.Maybe(Nat) -> Bool)
  Game.Bq.ilvreq (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.ilvreq)
   law Bq.ilvreq:
     (@+k_0: Nat -> Nat)
  Game.Bq.istreq (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.istreq)
   law Bq.istreq:
     (@+k_0: Nat -> Nat)
  Game.Bq.iagireq (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.iagireq)
   law Bq.iagireq:
     (@+k_0: Nat -> Nat)
  Game.Bq.ivitreq (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.ivitreq)
   law Bq.ivitreq:
     (@+k_0: Nat -> Nat)
  Game.Bq.Bool.and (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bool.and)
   law Bq.Bool.and:
     (@+a_0: Bool -> (@+b_1: Bool -> Bool))
  Game.Bq.can_wear (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.can_wear)
   law Bq.can_wear:
     (@+k_0: Nat -> (@+lv_1: Nat -> (@+str_2: Nat -> (@+agi_3: Nat -> (@+vit_4: Nat -> Bool)))))
  Game.Bq.Bag.le (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bag.le)
   law Bq.Bag.le:
     (@+a_0: Bq.Bag -> (@+b_1: Bq.Bag -> Bool))
  Game.Bq.equip_ok (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.equip_ok)
   law Bq.equip_ok:
     (@+k_0: Nat -> (@+h_1: Bq.Hero -> Bool))
  Game.Bq.slot_of (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.slot_of)
   law Bq.slot_of:
     (@+h_0: Bq.Hero -> (@+s_1: Bq.ISlot -> Bq.Maybe(Nat)))
  Game.Bq.Bool.not (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bool.not)
   law Bq.Bool.not:
     (@+a_0: Bool -> Bool)
  Game.Bq.unequip_ok (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.unequip_ok)
   law Bq.unequip_ok:
     (@+s_0: Bq.ISlot -> (@+h_1: Bq.Hero -> Bool))
  Game.Bq.Nat.lt (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Nat.lt)
   law Bq.Nat.lt:
     (@+a_0: Nat -> (@+b_1: Nat -> Bool))
  Game.Bq.buy_ok (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.buy_ok)
   law Bq.buy_ok:
     (@+k_0: Nat -> (@+h_1: Bq.Hero -> Bool))
  Game.Bq.quaff_ok (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.quaff_ok)
   law Bq.quaff_ok:
     (@+h_0: Bq.Hero -> Bool)
  Game.Bq.alloc_ok (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.alloc_ok)
   law Bq.alloc_ok:
     (@+h_0: Bq.Hero -> Bool)
  Game.Bq.hop_ok (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.hop_ok)
   law Bq.hop_ok:
     (@+op_0: Bq.HOp -> (@+h_1: Bq.Hero -> Bool))
  Game.Bq.hero_step (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.hero_step)
   law Bq.hero_step:
     (@+op_0: Bq.HOp -> (@+h_1: Bq.Hero -> Bq.Hero))
  Game.Bq.Nat.mul (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Nat.mul)
   law Bq.Nat.mul:
     (@+a_0: Nat -> (@+b_1: Nat -> Nat))
  Game.Bq.Nat.dbl (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Nat.dbl)
   law Bq.Nat.dbl:
     (@+n_0: Nat -> Nat)
  Game.Bq.Nat.pred (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Nat.pred)
   law Bq.Nat.pred:
     (@+n_0: Nat -> Nat)
  Game.Bq.max_hp (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.max_hp)
   law Bq.max_hp:
     (@+lv_0: Nat -> (@+vit_1: Nat -> Nat))
  Game.Bq.crit_dbl (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.crit_dbl)
   law Bq.crit_dbl:
     (@+crit_0: Bool -> (@+raw_1: Nat -> Nat))
  Game.Bq.nmin (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.nmin)
   law Bq.nmin:
     (@+a_0: Nat -> (@+b_1: Nat -> Nat))
  Game.Bq.nmax (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.nmax)
   law Bq.nmax:
     (@+a_0: Nat -> (@+b_1: Nat -> Nat))
  Game.Bq.DMG_CAP (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.DMG_CAP)
   law Bq.DMG_CAP:
     Nat
  Game.Bq.damage (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.damage)
   law Bq.damage:
     (@+watk_0: Nat -> (@+str_1: Nat -> (@+df_2: Nat -> (@+crit_3: Bool -> Nat))))
  Game.Bq.iatk (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.iatk)
   law Bq.iatk:
     (@+k_0: Nat -> Nat)
  Game.Bq.fresh_hero (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.fresh_hero)
   law Bq.fresh_hero:
     Bq.Hero
  Game.Bq.idf (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.idf)
   law Bq.idf:
     (@+k_0: Nat -> Nat)
  Game.Bq.mob_damage (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.mob_damage)
   law Bq.mob_damage:
     (@+matk_0: Nat -> (@+df_1: Nat -> (@+maxhp_2: Nat -> Nat)))
  Game.Bq.Dir (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Dir)
   type Bq.Dir is Data:
     Bq.Dir.DU{}
     Bq.Dir.DD{}
     Bq.Dir.DL{}
     Bq.Dir.DR{}
  Game.Bq.walk_x (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.walk_x)
   law Bq.walk_x:
     (@+w_0: Nat -> (@+x_1: Nat -> (@+d_2: Bq.Dir -> Nat)))
  Game.Bq.walk_y (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.walk_y)
   law Bq.walk_y:
     (@+h_0: Nat -> (@+y_1: Nat -> (@+d_2: Bq.Dir -> Nat)))
  Game.Bq.Pair.Pair (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Pair.Pair)
   law Bq.Pair.Pair:
     (@-A_0: Data -> (@-B_1: (@-__1: A_0 -> Data) -> Data))
  Game.Bq.walk (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.walk)
   law Bq.walk:
     (@+w_0: Nat -> (@+h_1: Nat -> (@+x_2: Nat -> (@+y_3: Nat -> (@+d_4: Bq.Dir -> Bq.Pair.Pair(Nat, (__5 => Nat)))))))
  Game.Bq.rejected_op_is_noop (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.rejected_op_is_noop)
   law Bq.rejected_op_is_noop:
     (@+op_0: Bq.HOp -> (@+h_1: Bq.Hero -> (@+__2: {Bq.hop_ok(op_0, h_1) == False{} : Bool} -> {Bq.hero_step(op_0, h_1) == h_1 : Bq.Hero})))
  Game.Bq.gear_bag (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.gear_bag)
   law Bq.gear_bag:
     (@+wea_0: Bq.Maybe(Nat) -> (@+arm_1: Bq.Maybe(Nat) -> (@+hel_2: Bq.Maybe(Nat) -> (@+chm_3: Bq.Maybe(Nat) -> Bq.Bag))))
  Game.Bq.census (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.census)
   law Bq.census:
     (@+h_0: Bq.Hero -> Bq.Bag)
  Game.Bq.Nat.add_zero (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Nat.add_zero)
   law Bq.Nat.add_zero:
     (@+a_0: Nat -> {Bq.Nat.add(a_0, 0n) == a_0 : Nat})
  Game.Bq.Nat.add_succ (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Nat.add_succ)
   law Bq.Nat.add_succ:
     (@+a_0: Nat -> (@+b_1: Nat -> {Bq.Nat.add(a_0, Succ{b_1}) == Succ{Bq.Nat.add(a_0, b_1)} : Nat}))
  Game.Bq.Nat.add_comm (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Nat.add_comm)
   law Bq.Nat.add_comm:
     (@+a_0: Nat -> (@+b_1: Nat -> {Bq.Nat.add(a_0, b_1) == Bq.Nat.add(b_1, a_0) : Nat}))
  Game.Bq.Bag.add_nil (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bag.add_nil)
   law Bq.Bag.add_nil:
     (@+a_0: Bq.Bag -> {Bq.Bag.add(a_0, Nil{}) == a_0 : Bq.Bag})
  Game.Bq.Bag.add_comm (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bag.add_comm)
   law Bq.Bag.add_comm:
     (@+a_0: Bq.Bag -> (@+b_1: Bq.Bag -> {Bq.Bag.add(a_0, b_1) == Bq.Bag.add(b_1, a_0) : Bq.Bag}))
  Game.Bq.Nat.add_assoc (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Nat.add_assoc)
   law Bq.Nat.add_assoc:
     (@+a_0: Nat -> (@+b_1: Nat -> (@+c_2: Nat -> {Bq.Nat.add(Bq.Nat.add(a_0, b_1), c_2) == Bq.Nat.add(a_0, Bq.Nat.add(b_1, c_2)) : Nat})))
  Game.Bq.Bag.add_assoc (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bag.add_assoc)
   law Bq.Bag.add_assoc:
     (@+a_0: Bq.Bag -> (@+b_1: Bq.Bag -> (@+c_2: Bq.Bag -> {Bq.Bag.add(Bq.Bag.add(a_0, b_1), c_2) == Bq.Bag.add(a_0, Bq.Bag.add(b_1, c_2)) : Bq.Bag})))
  Game.Bq.bag_swap (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.bag_swap)
   law Bq.bag_swap:
     (@+x_0: Bq.Bag -> (@+y_1: Bq.Bag -> (@+z_2: Bq.Bag -> {Bq.Bag.add(x_0, Bq.Bag.add(y_1, z_2)) == Bq.Bag.add(y_1, Bq.Bag.add(x_0, z_2)) : Bq.Bag})))
  Game.Bq.Bool.BoolD (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bool.BoolD)
   law Bq.Bool.BoolD:
     (@+x_0: Bool -> (@tc_1: Data -> (@fc_2: Data -> Data)))
  Game.Bq.Bool.false_ne_true (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bool.false_ne_true)
   law Bq.Bool.false_ne_true:
     (@+e_0: {False{} == True{} : Bool} -> Empty)
  Game.Bq.Nat.add_sub_cancel (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Nat.add_sub_cancel)
   law Bq.Nat.add_sub_cancel:
     (@+x_0: Nat -> (@+y_1: Nat -> (@+__2: {Bq.Nat.le(x_0, y_1) == True{} : Bool} -> {Bq.Nat.add(x_0, Bq.Nat.sub(y_1, x_0)) == y_1 : Nat})))
  Game.Bq.Bool.and_l (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bool.and_l)
   law Bq.Bool.and_l:
     (@+x_0: Bool -> (@+y_1: Bool -> (@+e_2: {Bq.Bool.and(x_0, y_1) == True{} : Bool} -> {x_0 == True{} : Bool})))
  Game.Bq.Bool.and_r (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bool.and_r)
   law Bq.Bool.and_r:
     (@+x_0: Bool -> (@+y_1: Bool -> (@+e_2: {Bq.Bool.and(x_0, y_1) == True{} : Bool} -> {y_1 == True{} : Bool})))
  Game.Bq.Bag.add_sub_cancel (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bag.add_sub_cancel)
   law Bq.Bag.add_sub_cancel:
     (@+a_0: Bq.Bag -> (@+b_1: Bq.Bag -> (@+__2: {Bq.Bag.le(a_0, b_1) == True{} : Bool} -> {Bq.Bag.add(a_0, Bq.Bag.sub(b_1, a_0)) == b_1 : Bq.Bag})))
  Game.Bq.equip_shuffle (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.equip_shuffle)
   law Bq.equip_shuffle:
     (@+i_0: Bq.Bag -> (@+k1_1: Bq.Bag -> (@+r_2: Bq.Bag -> (@+has_3: {Bq.Bag.le(k1_1, i_0) == True{} : Bool} -> {Bq.Bag.add(Bq.Bag.sub(i_0, k1_1), Bq.Bag.add(k1_1, r_2)) == Bq.Bag.add(i_0, r_2) : Bq.Bag}))))
  Game.Bq.equip_shuffle_chm (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.equip_shuffle_chm)
   law Bq.equip_shuffle_chm:
     (@+i_0: Bq.Bag -> (@+k1_1: Bq.Bag -> (@+w_2: Bq.Bag -> (@+a_3: Bq.Bag -> (@+hb_4: Bq.Bag -> (@+has_5: {Bq.Bag.le(k1_1, i_0) == True{} : Bool} -> {Bq.Bag.add(Bq.Bag.sub(i_0, k1_1), Bq.Bag.add(w_2, Bq.Bag.add(a_3, Bq.Bag.add(hb_4, k1_1)))) == Bq.Bag.add(i_0, Bq.Bag.add(w_2, Bq.Bag.add(a_3, Bq.Bag.add(hb_4, Nil{})))) : Bq.Bag}))))))
  Game.Bq.equip_preserves_census (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.equip_preserves_census)
   law Bq.equip_preserves_census:
     (@+k_0: Nat -> (@+h_1: Bq.Hero -> {Bq.census(Bq.hero_step(Bq.HOp.Equip{k_0}, h_1)) == Bq.census(h_1) : Bq.Bag}))
  Game.Bq.unequip_shuffle (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.unequip_shuffle)
   law Bq.unequip_shuffle:
     (@+i_0: Bq.Bag -> (@+k1_1: Bq.Bag -> (@+r_2: Bq.Bag -> {Bq.Bag.add(Bq.Bag.add(k1_1, i_0), r_2) == Bq.Bag.add(i_0, Bq.Bag.add(k1_1, r_2)) : Bq.Bag})))
  Game.Bq.unequip_shuffle2 (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.unequip_shuffle2)
   law Bq.unequip_shuffle2:
     (@+i_0: Bq.Bag -> (@+k1_1: Bq.Bag -> (@+w_2: Bq.Bag -> (@+g_3: Bq.Bag -> {Bq.Bag.add(Bq.Bag.add(k1_1, i_0), Bq.Bag.add(w_2, g_3)) == Bq.Bag.add(i_0, Bq.Bag.add(w_2, Bq.Bag.add(k1_1, g_3))) : Bq.Bag}))))
  Game.Bq.unequip_shuffle3 (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.unequip_shuffle3)
   law Bq.unequip_shuffle3:
     (@+i_0: Bq.Bag -> (@+k1_1: Bq.Bag -> (@+w_2: Bq.Bag -> (@+a_3: Bq.Bag -> (@+g_4: Bq.Bag -> {Bq.Bag.add(Bq.Bag.add(k1_1, i_0), Bq.Bag.add(w_2, Bq.Bag.add(a_3, g_4))) == Bq.Bag.add(i_0, Bq.Bag.add(w_2, Bq.Bag.add(a_3, Bq.Bag.add(k1_1, g_4)))) : Bq.Bag})))))
  Game.Bq.unequip_shuffle4 (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.unequip_shuffle4)
   law Bq.unequip_shuffle4:
     (@+i_0: Bq.Bag -> (@+k1_1: Bq.Bag -> (@+w_2: Bq.Bag -> (@+a_3: Bq.Bag -> (@+hb_4: Bq.Bag -> {Bq.Bag.add(Bq.Bag.add(k1_1, i_0), Bq.Bag.add(w_2, Bq.Bag.add(a_3, Bq.Bag.add(hb_4, Nil{})))) == Bq.Bag.add(i_0, Bq.Bag.add(w_2, Bq.Bag.add(a_3, Bq.Bag.add(hb_4, k1_1)))) : Bq.Bag})))))
  Game.Bq.unequip_preserves_census (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.unequip_preserves_census)
   law Bq.unequip_preserves_census:
     (@+s_0: Bq.ISlot -> (@+h_1: Bq.Hero -> {Bq.census(Bq.hero_step(Bq.HOp.Unequip{s_0}, h_1)) == Bq.census(h_1) : Bq.Bag}))
  Game.Bq.transfer (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.transfer)
   law Bq.transfer:
     (@+op_0: Bq.HOp -> Bool)
  Game.Bq.transfers (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.transfers)
   law Bq.transfers:
     (@+ops_0: List<&2, Bq.HOp> -> Bool)
  Game.Bq.hero_run (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.hero_run)
   law Bq.hero_run:
     (@+ops_0: List<&2, Bq.HOp> -> (@+h_1: Bq.Hero -> Bq.Hero))
  Game.Bq.transfers_preserve_census (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.transfers_preserve_census)
   law Bq.transfers_preserve_census:
     (@+ops_0: List<&2, Bq.HOp> -> (@+__1: {Bq.transfers(ops_0) == True{} : Bool} -> (@+h_2: Bq.Hero -> {Bq.census(Bq.hero_run(ops_0, h_2)) == Bq.census(h_2) : Bq.Bag})))
  Game.Bq.buy_mints_exactly_one (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.buy_mints_exactly_one)
   law Bq.buy_mints_exactly_one:
     (@+k_0: Nat -> (@+h_1: Bq.Hero -> (@+__2: {Bq.buy_ok(k_0, h_1) == True{} : Bool} -> {Bq.census(Bq.hero_step(Bq.HOp.Buy{k_0}, h_1)) == Bq.Bag.add(Bq.one(k_0), Bq.census(h_1)) : Bq.Bag})))
  Game.Bq.buy_burns_exact_gold (https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.buy_burns_exact_gold)
   law Bq.buy_burns_exact_gold:
     (@+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})))
More: https://jend.leeeet.dev/packages/gralha-bendquest.txt?definitions_offset=100