getVarWithLeastOccs — Mathlib

Lean4

/-- Search for the AC-variable (`Entry.acVar`) with the least occurrences in the state. -/
def getVarWithLeastOccs (ccs : CCState) (e : ACApps) (inLHS : Bool) : Option Expr :=
  match e with
  | .apps _ args =>
    Id.run
      (do
        let mut r := args[0]?
        let mut numOccs := r.casesOn 0 fun r' => ccs.getNumROccs r' inLHS
        for hi : i in [1:args.size]do
          if args[i] != (args[i - 1]'(Nat.lt_of_le_of_lt (i.sub_le 1) hi.2.1)) then
            let currOccs := ccs.getNumROccs args[i] inLHS
            if currOccs < numOccs then
              r := args[i]
              numOccs := currOccs
        return r)
  | .ofExpr e => e

Похожие утверждения