Ide.Plugin.Tactic.TestTypes

Documentation

data TacticCommand

The list of tactics exposed to the outside world. These are attached to actual tactics via commandTactic and are contextually provided to the editor via commandProvider.

Constructors

Auto

Intros

Destruct

Homomorphism

DestructLambdaCase

HomomorphismLambdaCase

Instances

Bounded TacticCommand

Defined in Ide.Plugin.Tactic.TestTypes

Methods

minBound :: TacticCommand

maxBound :: TacticCommand

Enum TacticCommand

Defined in Ide.Plugin.Tactic.TestTypes

Methods

succ :: TacticCommand -> TacticCommand

pred :: TacticCommand -> TacticCommand

toEnum :: Int -> TacticCommand

fromEnum :: TacticCommand -> Int

enumFrom :: TacticCommand -> [TacticCommand]

enumFromThen :: TacticCommand -> TacticCommand -> [TacticCommand]

enumFromTo :: TacticCommand -> TacticCommand -> [TacticCommand]

enumFromThenTo :: TacticCommand -> TacticCommand -> TacticCommand -> [TacticCommand]

Eq TacticCommand

Defined in Ide.Plugin.Tactic.TestTypes

Methods

(==) :: TacticCommand -> TacticCommand -> Bool

(/=) :: TacticCommand -> TacticCommand -> Bool

Ord TacticCommand

Defined in Ide.Plugin.Tactic.TestTypes

Methods

compare :: TacticCommand -> TacticCommand -> Ordering

(<) :: TacticCommand -> TacticCommand -> Bool

(<=) :: TacticCommand -> TacticCommand -> Bool

(>) :: TacticCommand -> TacticCommand -> Bool

(>=) :: TacticCommand -> TacticCommand -> Bool

max :: TacticCommand -> TacticCommand -> TacticCommand

min :: TacticCommand -> TacticCommand -> TacticCommand

Show TacticCommand

Defined in Ide.Plugin.Tactic.TestTypes

Methods

showsPrec :: Int -> TacticCommand -> ShowS

show :: TacticCommand -> String

showList :: [TacticCommand] -> ShowS

tacticTitle :: TacticCommand -> Text -> Text

Generate a title for the command.