Agda.Auto.Options

Documentation

data Mode

Constructors

MNormal Bool Bool

MCaseSplit

MRefine Bool

data AutoHintMode

Constructors

AHMNone

AHMModule

type Hints = [String]

newtype TimeOut

Constructors

TimeOut

Fields

• getTimeOut :: Int

Instances

Show TimeOut

Defined in Agda.Auto.Options

Methods

showsPrec :: Int -> TimeOut -> ShowS

show :: TimeOut -> String

showList :: [TimeOut] -> ShowS

data AutoOptions

Options for Auto, default value and lenses

Constructors

AutoOptions

Fields

• autoHints :: Hints
• autoTimeOut :: TimeOut
• autoPick :: Int
• autoMode :: Mode
• autoHintMode :: AutoHintMode

initAutoOptions :: AutoOptions

aoHints :: Lens' AutoOptions Hints

aoTimeOut :: Lens' AutoOptions TimeOut

aoPick :: Lens' AutoOptions Int

aoMode :: Lens' AutoOptions Mode

aoHintMode :: Lens' AutoOptions AutoHintMode

data AutoToken

Tokenising the input (makes parseArgs cleaner)

Constructors

M

C

R

D

L

T String

S Int

H String

autoTokens :: [String] -> [AutoToken]

parseTime :: String -> Int

parseArgs :: String -> AutoOptions