/root/interactive/lean/phase5/ThresholdNet.lean:173:54: warning: unused variable `hg` Note: This linter can be disabled with `set_option linter.unusedVariables false` 'NimAudit.ThresholdNet.sum_range_pos' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.orGate_eval' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.constGate_eval' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.orGate_valid' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.constGate_valid' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.orGate_fanin' depends on axioms: [propext] 'NimAudit.ThresholdNet.constGate_fanin' does not depend on any axioms 'NimAudit.ThresholdNet.lvlL_eq' does not depend on any axioms 'NimAudit.ThresholdNet.lvl_fhom' depends on axioms: [propext] 'NimAudit.ThresholdNet.lvl_le' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.lvlL_le' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.run_take' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.run_getD' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.rd_take' depends on axioms: [propext] 'NimAudit.ThresholdNet.lvlAlg_pos' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.lv_pos' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.getD_eq_getElem'' depends on axioms: [propext] 'NimAudit.ThresholdNet.vl_eq' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.lv_eq' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.rdv_take' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.rdl_take' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.evalLayer_at' depends on axioms: [propext] 'NimAudit.ThresholdNet.listMax_ge' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.vl_inp' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.vl_cst' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.vl_neg' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.vl_disj' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.vl_conj' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.lv_inp' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.lv_cst' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.lv_neg' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.lv_disj' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.lv_conj' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.child_lv' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.decide_or1' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.ThresholdNet.ys_spec' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.ThresholdNet.evalNet_append' does not depend on any axioms 'NimAudit.ThresholdNet.evalNet_layers' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.outs_range' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.ThresholdNet.outs_length' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.prog_length' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.valAlg_fhom' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.outs_val' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.outs_lv' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.compileF_eval' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.ThresholdNet.compileF_eval_out' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.compileF_valid' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.compileF_wired' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.compileF_length' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.cs_le_prog' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.compileF_bounded' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.compileF_gates' depends on axioms: [propext, Quot.sound] 'NimAudit.ThresholdNet.compileF_spec' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.ThresholdNet.compileF_fixed_grid' depends on axioms: [propext, Classical.choice, Quot.sound]