instOrdACApps — Mathlib

Lean4
/-- Ordering on `ACApps` sorts `.ofExpr` before `.apps`, and sorts `.apps` by function symbol,
  then by shortlex order. -/
scoped instance : Ord ACApps where
  compare
    | .ofExpr a, .ofExpr b => compare a b
    | .ofExpr _, .apps _ _ => .lt
    | .apps _ _, .ofExpr _ => .gt
    | .apps op₁ args₁, .apps op₂ args₂ =>
      compare op₁ op₂ |>.then <|
        compare args₁.size args₂.size |>.dthen fun hs =>
          Id.run
            (do
              have hs := eq_of_beq <| Std.LawfulBEqCmp.compare_eq_iff_beq.mp hs
              for hi : i in [:args₁.size]do
                have hi := hi.right
                let o := compare args₁[i] (args₂[i]'(hs ▸ hi.1))
                if o != .eq then
                  return o
              return .eq)
Похожие утверждения