forked from leanprover/lean4
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathTactic.lean
31 lines (31 loc) · 990 Bytes
/
Tactic.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.Tactic.Intro
import Lean.Meta.Tactic.Assumption
import Lean.Meta.Tactic.Contradiction
import Lean.Meta.Tactic.Apply
import Lean.Meta.Tactic.Revert
import Lean.Meta.Tactic.Clear
import Lean.Meta.Tactic.Assert
import Lean.Meta.Tactic.Rewrite
import Lean.Meta.Tactic.Generalize
import Lean.Meta.Tactic.Replace
import Lean.Meta.Tactic.Induction
import Lean.Meta.Tactic.Cases
import Lean.Meta.Tactic.ElimInfo
import Lean.Meta.Tactic.Delta
import Lean.Meta.Tactic.Constructor
import Lean.Meta.Tactic.Simp
import Lean.Meta.Tactic.AuxLemma
import Lean.Meta.Tactic.SplitIf
import Lean.Meta.Tactic.Split
import Lean.Meta.Tactic.Cleanup
import Lean.Meta.Tactic.Unfold
import Lean.Meta.Tactic.Rename
import Lean.Meta.Tactic.LinearArith
import Lean.Meta.Tactic.AC
import Lean.Meta.Tactic.Refl
import Lean.Meta.Tactic.Congr