Agda.Mimer.Options

Documentation

type MilliSeconds = Integer

data HintMode

Constructors

Unqualified

AllModules

Module

NoHints

Instances

Pretty HintMode

Defined in Agda.Mimer.Options

Methods

pretty :: HintMode -> Doc

prettyPrec :: Int -> HintMode -> Doc

prettyList :: [HintMode] -> Doc

Show HintMode

Defined in Agda.Mimer.Options

Methods

showsPrec :: Int -> HintMode -> ShowS

show :: HintMode -> String

showList :: [HintMode] -> ShowS

Eq HintMode

Defined in Agda.Mimer.Options

Methods

(==) :: HintMode -> HintMode -> Bool

(/=) :: HintMode -> HintMode -> Bool

data Options

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

Show Options

Defined in Agda.Mimer.Options

Methods

showsPrec :: Int -> Options -> ShowS

show :: Options -> String

showList :: [Options] -> ShowS

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

parseTime :: String -> Int

hintExprToQName :: Expr -> Maybe QName

firstOr :: a -> [a] -> a

data Token

Constructors

T String

M

U

C

L

S String

H String

Instances

Show Token

Defined in Agda.Mimer.Options

Methods

showsPrec :: Int -> Token -> ShowS

show :: Token -> String

showList :: [Token] -> ShowS

Eq Token

Defined in Agda.Mimer.Options

Methods

(==) :: Token -> Token -> Bool

(/=) :: Token -> Token -> Bool

readTokens :: [String] -> [Token]