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

Safe Haskell | None
Language | Haskell2010

Agda.Mimer.Options

# Documentation

type MilliSeconds = Integer Source #

data HintMode Source #

Constructors

Unqualified |
AllModules |
Module |
NoHints |

#### Instances

Instances details

Pretty HintMode Source # |
Instance details Defined in Agda.Mimer.Options Methods pretty :: HintMode -> Doc Source # prettyPrec :: Int -> HintMode -> Doc Source # prettyList :: [HintMode] -> Doc Source #
Show HintMode Source # |
Instance details Defined in Agda.Mimer.Options Methods showsPrec :: Int -> HintMode -> ShowS Source # show :: HintMode -> String Source # showList :: [HintMode] -> ShowS Source #
Eq HintMode Source # |
Instance details Defined in Agda.Mimer.Options Methods (==) :: HintMode -> HintMode -> Bool Source # (/=) :: HintMode -> HintMode -> Bool Source #

data Options Source #

Constructors

Options |

Fields

- optTimeout :: MilliSeconds
- optHintMode :: HintMode
- optSkip :: Int

  Skip the first this many solutions

- optList :: Bool

  List solutions instead of filling the hole

- optExplicitHints :: [QName]

#### Instances

Instances details

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

parseOptions :: InteractionId -> Range -> String -> TCM Options Source #

parseTime :: String -> Int Source #

hintExprToQName :: Expr -> Maybe QName Source #

firstOr :: a -> [a] -> a Source #

data Token Source #

Constructors

T String |
M |
U |
C |
L |
S String |
H String |

#### Instances

Instances details

Show Token Source # |
Instance details Defined in Agda.Mimer.Options Methods showsPrec :: Int -> Token -> ShowS Source # show :: Token -> String Source # showList :: [Token] -> ShowS Source #
Eq Token Source # |
Instance details Defined in Agda.Mimer.Options Methods (==) :: Token -> Token -> Bool Source # (/=) :: Token -> Token -> Bool Source #

readTokens :: [String] -> [Token] Source #