Agda-2.6.20240714: 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 #