Lean.Meta.isDefEq doesn't know (3 = 3) = true?

Stream: lean4

[Tanner Swett]

I'm trying to write an #assert_eq command that throws an error if its two arguments are not definitionally equal expressions. It uses Lean.meta.isDefEq to try to determine if the arguments are definitionally equal or not. However, isDefEq seems to be telling me that the expression (3 = 3 : Bool) isn't definitionally equal to the expression true. Why not?

Part of me thinks I need to reduce the input expressions, but isn't isDefEq supposed to usually be able to determine whether or not two expressions are definitionally equal without actually reducing them first?

Here's my code:

elab "#assert_eq " l:term:arg r:term:arg : command => do
  let l_equals_r ← liftTermElabM <| do
    let l_value ← elabTerm (expectedType? := none) l
    let r_value ← elabTerm (expectedType? := none) r
    Lean.Meta.isDefEq l_value r_value

  if not l_equals_r then
    throwErrorAt r "The value{Lean.indentD l}\nis not definitionally equal to the value{Lean.indentD r}"

#assert_eq (3 = 3 : Bool) true

[Kyle Miller]

It's probably because you're not synthesizing metavariables before doing the defeq check (like with synthesizeSyntheticMVarsNoPostponing). You need this to get Lean to commit to 3 being a Nat, which requires it to use a default OfNat instance.

[Kyle Miller]

There's already such a command in Std4 by the way: https://github.com/leanprover/std4/blob/main/Std/Tactic/GuardExpr.lean#L197

[Tanner Swett]

Sticking a synthesizeSyntheticMVarsNoPostponing in there seems to do the trick! Thank you!

[Tanner Swett]

(also, since I plan to do quite a lot of metaprogramming, I figure it's a good idea to try implementing the simple stuff myself)