Lean4
/-- If `e` is of the form `op e₁ e₂` where `op` is an associative and commutative binary operator,
return the canonical form of `op`. -/
def isAC (e : Expr) : CCM (Option Expr) := do
let .app (.app op _) _ := e |
return none
let ccs ← get
if let some cop := ccs.canOps[op]? then
let some b := ccs.opInfo[cop]? |
throwError"opInfo should contain all canonical operators in canOps"
return bif b then some cop else none
for (cop, b) in ccs.opInfo do
if ← pureIsDefEq op cop then
modify fun _ => { ccs with canOps := ccs.canOps.insert op cop }
return bif b then some cop else none
let b ←
try
let aop ← mkAppM ``Std.Associative #[op]
let some _ ← synthInstance? aop |
failure
let cop ← mkAppM ``Std.Commutative #[op]
let some _ ← synthInstance? cop |
failure
pure true
catch _ =>
pure false
modify fun _ =>
{ ccs with
canOps := ccs.canOps.insert op op
opInfo := ccs.opInfo.insert op b }
return bif b then some op else none
