Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl. 
/-
Tactics for the project
-/

import Init.Tactics
import Mathlib.Tactic.Linarith.Frontend
import Std.Tactic.RCases

open Lean Elab Parser Term Meta Macro Std.Tactic.RCases

/--
`dwi t` (deal with it) is a tactic that runs `t` and then tries to 
solve the goal using `contradiction`, `assumption`, `simp`, and `simpa`.
-/
syntax "dwi " "{" 
tactic: Category
tactic "}" : 
tactic: Category
tactic

macro_rules
  | `(tactic| dwi { $
t: ?m.117
t }) => 
    `(tactic| $
t: ?m.117
t <;> try { first | contradiction | assumption | simp | simpa })