Agda-2.6.0.1: 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 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

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

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

aoTimeOut :: Lens' TimeOut AutoOptions Source #

aoPick :: Lens' Int AutoOptions Source #

aoMode :: Lens' Mode AutoOptions Source #

aoHintMode :: Lens' AutoHintMode AutoOptions 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 #