Simp as a command / function?

Stream: new members

[Mark Aagaard]

I'm using Lean in an intro to logic course for computer engineers and would like to demonstrate term simplification to the students. Is it feasible to wrap some code around the simp tactic to create a command or function that displays the simplified form of a term? If yes, then any pointers on where to start would be great.

For example:
variable (a b : Bool)

#simp a && b && true
a && b

-mark

[Kyle Miller]

If you're using mathlib, it's just an import away :smile:

import Mathlib.Tactic.Common

variable (a b : Bool)

#simp a && b && true
-- a && b

[Kyle Miller]

If you aren't using Mathlib, you can copy Mathlib/Tactic/Conv.lean and delete the import Mathlib.Init import.

[Mark Aagaard]

That's great. Thanks!

-mark