A Basic Tactic
This is a very basic tactic that does nothing. This is just to show how to define a tactic in Lean.
open Lean Elab Tactic
elab "hello_tactic" : tactic => do
return
example : 1 = 1 := ⊢ 1 = 1
⊢ 1 = 1
All goals completed! 🐙
This is a very basic tactic that does nothing. This is just to show how to define a tactic in Lean.
open Lean Elab Tactic
elab "hello_tactic" : tactic => do
return
example : 1 = 1 := ⊢ 1 = 1
⊢ 1 = 1
All goals completed! 🐙