Agda-2.6.5: 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 # show :: HintMode -> String # showList :: [HintMode] -> ShowS #
Eq HintMode Source #
Instance details Defined in Agda.Mimer.Options Methods (==) :: HintMode -> HintMode -> Bool # (/=) :: HintMode -> HintMode -> Bool #

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 # show :: Options -> String # showList :: [Options] -> ShowS #

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 # show :: Token -> String # showList :: [Token] -> ShowS #
Eq Token Source #
Instance details Defined in Agda.Mimer.Options Methods (==) :: Token -> Token -> Bool # (/=) :: Token -> Token -> Bool #

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