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

Safe Haskell	Safe-Inferred
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' AutoOptions Hints
aoTimeOut :: Lens' AutoOptions TimeOut
aoPick :: Lens' AutoOptions Int
aoMode :: Lens' AutoOptions Mode
aoHintMode :: Lens' AutoOptions AutoHintMode
data AutoToken
- = M
- | C
- | R
- | D
- | L
- | T String
- | S Int
- | H String
autoTokens :: [String] -> [AutoToken]
parseTime :: String -> Int
parseArgs :: String -> AutoOptions

Documentation

data Mode Source #

Constructors

MNormal Bool Bool
MCaseSplit
MRefine Bool

data AutoHintMode Source #

Constructors

AHMNone
AHMModule

type Hints = [String] Source #

newtype TimeOut Source #

Constructors

TimeOut
Fields getTimeOut :: Int

Instances

Instances details

Show TimeOut Source #
Instance details Defined in Agda.Auto.Options Methods showsPrec :: Int -> TimeOut -> ShowS # show :: TimeOut -> String # showList :: [TimeOut] -> ShowS #

data AutoOptions Source #

Options for Auto, default value and lenses

Constructors

AutoOptions
Fields autoHints :: Hints autoTimeOut :: TimeOut autoPick :: Int autoMode :: Mode autoHintMode :: AutoHintMode

initAutoOptions :: AutoOptions Source #

aoHints :: Lens' AutoOptions Hints Source #

aoTimeOut :: Lens' AutoOptions TimeOut Source #

aoPick :: Lens' AutoOptions Int Source #

aoMode :: Lens' AutoOptions Mode Source #

aoHintMode :: Lens' AutoOptions AutoHintMode Source #

data AutoToken Source #

Tokenising the input (makes parseArgs cleaner)

Constructors

M
C
R
D
L
T String
S Int
H String

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

parseTime :: String -> Int Source #

parseArgs :: String -> AutoOptions Source #