Hi! What would be the shortest/cleanest way to check, within SML, whether within a given proof context, the simplifier would be able to prove two terms equal? In other words, given terms `s`

and `t`

of the same type, I'd like to know, in ML, whether

```
lemma: <s = t>
by simp
```

would succeed.

That's how I would do it:

```
ML‹
(*example values*)
val (s, t) = (@{cterm "0 :: nat"}, @{cterm "0 + 0 :: nat "})
val ctxt = @{context}
val cT = Thm.ctyp_of_cterm s
val goal = \<^instantiate>‹'a = cT and s and t in
cterm ‹Trueprop (s = t)› for s :: 'a and t›
val simp_tac = Simplifier.simp_tac ctxt |> SOLVED' |> HEADGOAL |> SINGLE
val thmOpt = Goal.init goal |> simp_tac |> Option.map Goal.conclude
val _ = @{print} thmOpt
›
```

Edit: fixed a line

Awesome, thank you @Kevin Kappelmann !

Last updated: Dec 07 2023 at 16:21 UTC