Documentation
LeanPool
.
Lentil
.
ProofMode
.
Tactics
Search
return to top
source
Imports
Init
LeanPool.Lentil.ProofMode.Tactics.Apply
LeanPool.Lentil.ProofMode.Tactics.Assumption
LeanPool.Lentil.ProofMode.Tactics.CheckGoalForm
LeanPool.Lentil.ProofMode.Tactics.Clear
LeanPool.Lentil.ProofMode.Tactics.CoalesceToPTL
LeanPool.Lentil.ProofMode.Tactics.Contradiction
LeanPool.Lentil.ProofMode.Tactics.Exists
LeanPool.Lentil.ProofMode.Tactics.Exit
LeanPool.Lentil.ProofMode.Tactics.Have
LeanPool.Lentil.ProofMode.Tactics.Intro
LeanPool.Lentil.ProofMode.Tactics.LeftRight
LeanPool.Lentil.ProofMode.Tactics.ModalityMisc
LeanPool.Lentil.ProofMode.Tactics.Monotone
LeanPool.Lentil.ProofMode.Tactics.Normalize
LeanPool.Lentil.ProofMode.Tactics.PurePred
LeanPool.Lentil.ProofMode.Tactics.RCases
LeanPool.Lentil.ProofMode.Tactics.Rename
LeanPool.Lentil.ProofMode.Tactics.Revert
LeanPool.Lentil.ProofMode.Tactics.Rewrite
LeanPool.Lentil.ProofMode.Tactics.Simp
LeanPool.Lentil.ProofMode.Tactics.Specialize
LeanPool.Lentil.ProofMode.Tactics.SplitAnds
LeanPool.Lentil.ProofMode.Tactics.Start
Imported by