Agda-2.5.4: A dependently typed functional programming language and proof assistant

Safe Haskell	Safe
Language	Haskell2010

Agda.Auto.Options

Synopsis

data Mode
- = MNormal Bool Bool
- | MCaseSplit
- | MRefine Bool
data AutoHintMode
- = AHMNone
- | AHMModule
type Hints = [String]
newtype TimeOut = TimeOut {
- getTimeOut :: Int
}
data AutoOptions = AutoOptions {
- autoHints :: Hints
- autoTimeOut :: TimeOut
- autoPick :: Int
- autoMode :: Mode
- autoHintMode :: AutoHintMode
}
initAutoOptions :: AutoOptions
aoHints :: Lens' Hints AutoOptions
aoTimeOut :: Lens' TimeOut AutoOptions
aoPick :: Lens' Int AutoOptions
aoMode :: Lens' Mode AutoOptions
aoHintMode :: Lens' AutoHintMode AutoOptions
data AutoToken
- = M
- | C
- | R
- | D
- | L
- | T Int
- | S Int
- | H String
autoTokens :: [String] -> [AutoToken]
parseArgs :: String -> AutoOptions

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 #
Instance details 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' Hints AutoOptions #

aoTimeOut :: Lens' TimeOut AutoOptions #

aoPick :: Lens' Int AutoOptions #

aoMode :: Lens' Mode AutoOptions #

aoHintMode :: Lens' AutoHintMode AutoOptions #

data AutoToken #

Tokenising the input (makes parseArgs cleaner)

Constructors

M
C
R
D
L
T Int
S Int
H String

autoTokens :: [String] -> [AutoToken] #

parseArgs :: String -> AutoOptions #