Hello World Tactic🔗

Contributors: AnirudhG07, Siddhartha Gadgil

A Basic Tactic🔗

This is a very basic tactic that does nothing. This is just to show how to define a tactic in Lean. Note that we should begin a tactic with Lean.Elab.Tactic.withMainContext to ensure that the tactic is executed in the context of the main goal.

open Lean Elab Tactic

elab "hello_tactic" : tactic =>
  withMainContext do
  return

example : 1 = 1 := by⊢ 1 = 1
  hello_tactic⊢ 1 = 1
  rflAll goals completed! 🐙