/root/interactive/lean/phase6/RolloutExec.lean:520:18: warning: unused variable `Q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
'NimAudit.RolloutExec.untilHalt_halted' depends on axioms: [propext]
'NimAudit.RolloutExec.rolloutWinner_none'' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.rolloutWinner_some'' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.untilHalt_spec' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.clock_ok' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.eval_mux' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.stepForms_length' depends on axioms: [propext]
'NimAudit.RolloutExec.polSpec_polBin' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.stepForms_board' depends on axioms: [propext]
'NimAudit.RolloutExec.stepForms_par' depends on axioms: [propext]
'NimAudit.RolloutExec.stepForms_halt' depends on axioms: [propext]
'NimAudit.RolloutExec.any_decode' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.eval_mvC' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.maxInput_decodeC' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.maxInput_getC_le' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.getD_set_nat' depends on axioms: [propext]
'NimAudit.RolloutExec.boardBits_set' depends on axioms: [propext]
'NimAudit.RolloutExec.bitStep_run' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.bitStep_reset' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.loopUntil_congr' depends on axioms: [propext]
'NimAudit.RolloutExec.rsStep_inv' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.loop_refines' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.execRoll_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.netStep_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.execRollN_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.execRollN_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.outBit_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.mhExec_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.mhExec_eq_mhMove' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.mhExecSel_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.mhExec_wins' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.mhExec_evals' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.rollCalls_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.mhSelect_calls' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.unbounded_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.depth_mux_le' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.size_mux' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.maxInput_mux' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.xor2_res' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.stepForms_res' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.stepLen_pos' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.step_leaves' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.stepF_tsize' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.step_ac0' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.step_net' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.mhWork_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.polyIn_comp' depends on axioms: [propext]
'NimAudit.RolloutExec.work_leaves' depends on axioms: [propext, Quot.sound]
'NimAudit.RolloutExec.mhWork_poly' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.RolloutExec.mhWork_poly_logB' depends on axioms: [propext, Classical.choice, Quot.sound]