defeq-elab.lean

import Lean.Elab.Command
open Lean

elab "#defeq " σ₁:term " =?= " σ₂:term : command =>
  Elab.Command.liftTermElabM (do
    let τ₁ ← Elab.Term.elabTerm σ₁ none
    let τ₂ ← Elab.Term.elabTerm σ₂ none
    unless (← Meta.isDefEq τ₁ τ₂) do throwError s!"{τ₁} ≠ {τ₂}")

#defeq [1, 2, 3, 4].reverse =?= [4, 3, 2, 1]

macro "#defeqEval " σ₁:term " =?= " σ₂:term : command =>
  `(#eval (unless ($σ₁ == $σ₂)
    do throwError s!"{$σ₁} ≠ {$σ₂}" : Elab.Command.CommandElabM Unit))

#defeqEval [1, 2, 3, 4].reverse =?= [4, 3, 2, 1]