Skip to content

HORIZON HASKELL Docs lts/ghc-10.0.x77a86622026-10-31Search packagesCtrl K

Theme: |

GHC 10.0.0.20260917 · lts/ghc-10.0.x · 77a8662 · 2026-10-31

ModuleAgda-2.8.0.2Haskell2010

Agda.Mimer.Options

Synopsis

type MilliSeconds
data HintMode
data Options
value parseOptions
value parseTime
value hintExprToQName
value firstOr
data Token
value readTokens

PackageAgda-2.8.0.2
Exports9
LanguageHaskell2010
LicenceMIT

typetype MilliSeconds = Integer

datadata HintMode

Unqualified AllModules Module NoHints

Instances3Eq, Show, Pretty

Eq HintModeDefined in Agda-2.8.0.2 · Agda.Mimer.Options
Show HintModeDefined in Agda-2.8.0.2 · Agda.Mimer.Options
Pretty HintModeDefined in Agda-2.8.0.2 · Agda.Mimer.Options

datadata Options

Constructors

Options
- optTimeout :: MilliSeconds
- optHintMode :: HintMode
- optSkip :: Int
  Skip the first this many solutions
- optList :: Bool
  List solutions instead of filling the hole
- optExplicitHints :: [QName]

Instances1Show

Show OptionsDefined in Agda-2.8.0.2 · Agda.Mimer.Options

valueparseOptions :: InteractionId -> Range -> String -> TCM Options

valueparseTime :: String -> Int

valuehintExprToQName :: Expr -> Maybe QName

valuefirstOr :: a -> [a] -> a

datadata Token

Constructors

T String
M
U
C
L
S String
H String

Instances2Eq, Show

Eq TokenDefined in Agda-2.8.0.2 · Agda.Mimer.Options
Show TokenDefined in Agda-2.8.0.2 · Agda.Mimer.Options

valuereadTokens :: [String] -> [Token]