Ide.Plugin.Tactic

A plugin that uses tactics to synthesize code

Documentation

descriptor :: PluginId -> PluginDescriptor IdeState

tacticTitle :: TacticCommand -> Text -> Text

Generate a title for the command.

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

DestructPun

Homomorphism

DestructLambdaCase

HomomorphismLambdaCase

DestructAll

UseDataCon

Refine

BeginMetaprogram

RunMetaprogram

Instances

Bounded TacticCommand

Defined in Wingman.Types

Methods

minBound :: TacticCommand

maxBound :: TacticCommand

Enum TacticCommand

Defined in Wingman.Types

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 Wingman.Types

Methods

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

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

Ord TacticCommand

Defined in Wingman.Types

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 Wingman.Types

Methods

showsPrec :: Int -> TacticCommand -> ShowS

show :: TacticCommand -> String

showList :: [TacticCommand] -> ShowS