Cornelis.Types.Agda

Documentation

data Rewrite

Constructors

AsIs

Instantiated

HeadNormal

Simplified

Normalised

Instances

Bounded Rewrite

Defined in Cornelis.Types.Agda

Methods

minBound :: Rewrite

maxBound :: Rewrite

Enum Rewrite

Defined in Cornelis.Types.Agda

Methods

succ :: Rewrite -> Rewrite

pred :: Rewrite -> Rewrite

toEnum :: Int -> Rewrite

fromEnum :: Rewrite -> Int

enumFrom :: Rewrite -> [Rewrite]

enumFromThen :: Rewrite -> Rewrite -> [Rewrite]

enumFromTo :: Rewrite -> Rewrite -> [Rewrite]

enumFromThenTo :: Rewrite -> Rewrite -> Rewrite -> [Rewrite]

Read Rewrite

Defined in Cornelis.Types.Agda

Methods

readsPrec :: Int -> ReadS Rewrite

readList :: ReadS [Rewrite]

readPrec :: ReadPrec Rewrite

readListPrec :: ReadPrec [Rewrite]

Show Rewrite

Defined in Cornelis.Types.Agda

Methods

showsPrec :: Int -> Rewrite -> ShowS

show :: Rewrite -> String

showList :: [Rewrite] -> ShowS

Eq Rewrite

Defined in Cornelis.Types.Agda

Methods

(==) :: Rewrite -> Rewrite -> Bool

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

Ord Rewrite

Defined in Cornelis.Types.Agda

Methods

compare :: Rewrite -> Rewrite -> Ordering

(<) :: Rewrite -> Rewrite -> Bool

(<=) :: Rewrite -> Rewrite -> Bool

(>) :: Rewrite -> Rewrite -> Bool

(>=) :: Rewrite -> Rewrite -> Bool

max :: Rewrite -> Rewrite -> Rewrite

min :: Rewrite -> Rewrite -> Rewrite

data ComputeMode

Constructors

DefaultCompute

HeadCompute

IgnoreAbstract

UseShowInstance

Instances

Bounded ComputeMode

Defined in Cornelis.Types.Agda

Methods

minBound :: ComputeMode

maxBound :: ComputeMode

Enum ComputeMode

Defined in Cornelis.Types.Agda

Methods

succ :: ComputeMode -> ComputeMode

pred :: ComputeMode -> ComputeMode

toEnum :: Int -> ComputeMode

fromEnum :: ComputeMode -> Int

enumFrom :: ComputeMode -> [ComputeMode]

enumFromThen :: ComputeMode -> ComputeMode -> [ComputeMode]

enumFromTo :: ComputeMode -> ComputeMode -> [ComputeMode]

enumFromThenTo :: ComputeMode -> ComputeMode -> ComputeMode -> [ComputeMode]

Read ComputeMode

Defined in Cornelis.Types.Agda

Methods

readsPrec :: Int -> ReadS ComputeMode

readList :: ReadS [ComputeMode]

readPrec :: ReadPrec ComputeMode

readListPrec :: ReadPrec [ComputeMode]

Show ComputeMode

Defined in Cornelis.Types.Agda

Methods

showsPrec :: Int -> ComputeMode -> ShowS

show :: ComputeMode -> String

showList :: [ComputeMode] -> ShowS

Eq ComputeMode

Defined in Cornelis.Types.Agda

Methods

(==) :: ComputeMode -> ComputeMode -> Bool

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

Ord ComputeMode

Defined in Cornelis.Types.Agda

Methods

compare :: ComputeMode -> ComputeMode -> Ordering

(<) :: ComputeMode -> ComputeMode -> Bool

(<=) :: ComputeMode -> ComputeMode -> Bool

(>) :: ComputeMode -> ComputeMode -> Bool

(>=) :: ComputeMode -> ComputeMode -> Bool

max :: ComputeMode -> ComputeMode -> ComputeMode

min :: ComputeMode -> ComputeMode -> ComputeMode

data UseForce

Constructors

WithForce

Ignore additional checks, like termination/positivity...

WithoutForce

Don't ignore any checks.

Instances

Read UseForce

Defined in Cornelis.Types.Agda

Methods

readsPrec :: Int -> ReadS UseForce

readList :: ReadS [UseForce]

readPrec :: ReadPrec UseForce

readListPrec :: ReadPrec [UseForce]

Show UseForce

Defined in Cornelis.Types.Agda

Methods

showsPrec :: Int -> UseForce -> ShowS

show :: UseForce -> String

showList :: [UseForce] -> ShowS

Eq UseForce

Defined in Cornelis.Types.Agda

Methods

(==) :: UseForce -> UseForce -> Bool

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

newtype InteractionId

Constructors

InteractionId

Fields

• interactionId :: Int

Instances

FromJSON InteractionId

Defined in Cornelis.Types.Agda

Methods

parseJSON :: Value -> Parser InteractionId

parseJSONList :: Value -> Parser [InteractionId]

omittedField :: Maybe InteractionId

ToJSON InteractionId

Defined in Cornelis.Types.Agda

Methods

toJSON :: InteractionId -> Value

toEncoding :: InteractionId -> Encoding

toJSONList :: [InteractionId] -> Value

toEncodingList :: [InteractionId] -> Encoding

omitField :: InteractionId -> Bool

Enum InteractionId

Defined in Cornelis.Types.Agda

Methods

succ :: InteractionId -> InteractionId

pred :: InteractionId -> InteractionId

toEnum :: Int -> InteractionId

fromEnum :: InteractionId -> Int

enumFrom :: InteractionId -> [InteractionId]

enumFromThen :: InteractionId -> InteractionId -> [InteractionId]

enumFromTo :: InteractionId -> InteractionId -> [InteractionId]

enumFromThenTo :: InteractionId -> InteractionId -> InteractionId -> [InteractionId]

Num InteractionId

Defined in Cornelis.Types.Agda

Methods

(+) :: InteractionId -> InteractionId -> InteractionId

(-) :: InteractionId -> InteractionId -> InteractionId

(*) :: InteractionId -> InteractionId -> InteractionId

negate :: InteractionId -> InteractionId

abs :: InteractionId -> InteractionId

signum :: InteractionId -> InteractionId

fromInteger :: Integer -> InteractionId

Read InteractionId

Defined in Cornelis.Types.Agda

Methods

readsPrec :: Int -> ReadS InteractionId

readList :: ReadS [InteractionId]

readPrec :: ReadPrec InteractionId

readListPrec :: ReadPrec [InteractionId]

Integral InteractionId

Defined in Cornelis.Types.Agda

Methods

quot :: InteractionId -> InteractionId -> InteractionId

rem :: InteractionId -> InteractionId -> InteractionId

div :: InteractionId -> InteractionId -> InteractionId

mod :: InteractionId -> InteractionId -> InteractionId

quotRem :: InteractionId -> InteractionId -> (InteractionId, InteractionId)

divMod :: InteractionId -> InteractionId -> (InteractionId, InteractionId)

toInteger :: InteractionId -> Integer

Real InteractionId

Defined in Cornelis.Types.Agda

Methods

toRational :: InteractionId -> Rational

Show InteractionId

Defined in Cornelis.Types.Agda

Methods

showsPrec :: Int -> InteractionId -> ShowS

show :: InteractionId -> String

showList :: [InteractionId] -> ShowS

Eq InteractionId

Defined in Cornelis.Types.Agda

Methods

(==) :: InteractionId -> InteractionId -> Bool

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

Ord InteractionId

Defined in Cornelis.Types.Agda

Methods

compare :: InteractionId -> InteractionId -> Ordering

(<) :: InteractionId -> InteractionId -> Bool

(<=) :: InteractionId -> InteractionId -> Bool

(>) :: InteractionId -> InteractionId -> Bool

(>=) :: InteractionId -> InteractionId -> Bool

max :: InteractionId -> InteractionId -> InteractionId

min :: InteractionId -> InteractionId -> InteractionId

type Command = Command' IOTCM

IOTCM commands.

type IntervalWithoutFile = AgdaInterval

data Command' a

Constructors

Command !a

A command.

Done

Stop processing commands.

Error String

An error message for a command that could not be parsed.

Instances

Show a => Show (Command' a)

Defined in Cornelis.Types.Agda

Methods

showsPrec :: Int -> Command' a -> ShowS

show :: Command' a -> String

showList :: [Command' a] -> ShowS

data Range' a

Constructors

NoRange

Range !a (Seq IntervalWithoutFile)

Instances

Foldable Range'

Defined in Cornelis.Types.Agda

Methods

fold :: Monoid m => Range' m -> m

foldMap :: Monoid m => (a -> m) -> Range' a -> m

foldMap' :: Monoid m => (a -> m) -> Range' a -> m

foldr :: (a -> b -> b) -> b -> Range' a -> b

foldr' :: (a -> b -> b) -> b -> Range' a -> b

foldl :: (b -> a -> b) -> b -> Range' a -> b

foldl' :: (b -> a -> b) -> b -> Range' a -> b

foldr1 :: (a -> a -> a) -> Range' a -> a

foldl1 :: (a -> a -> a) -> Range' a -> a

toList :: Range' a -> [a]

null :: Range' a -> Bool

length :: Range' a -> Int

elem :: Eq a => a -> Range' a -> Bool

maximum :: Ord a => Range' a -> a

minimum :: Ord a => Range' a -> a

sum :: Num a => Range' a -> a

product :: Num a => Range' a -> a

Traversable Range'

Defined in Cornelis.Types.Agda

Methods

traverse :: Applicative f => (a -> f b) -> Range' a -> f (Range' b)

sequenceA :: Applicative f => Range' (f a) -> f (Range' a)

mapM :: Monad m => (a -> m b) -> Range' a -> m (Range' b)

sequence :: Monad m => Range' (m a) -> m (Range' a)

Functor Range'

Defined in Cornelis.Types.Agda

Methods

fmap :: (a -> b) -> Range' a -> Range' b

(<$) :: a -> Range' b -> Range' a

Generic (Range' a)

Defined in Cornelis.Types.Agda

Associated Types

type Rep (Range' a) :: Type -> Type

Methods

from :: Range' a -> Rep (Range' a) x

to :: Rep (Range' a) x -> Range' a

Show a => Show (Range' a)

Defined in Cornelis.Types.Agda

Methods

showsPrec :: Int -> Range' a -> ShowS

show :: Range' a -> String

showList :: [Range' a] -> ShowS

Eq a => Eq (Range' a)

Defined in Cornelis.Types.Agda

Methods

(==) :: Range' a -> Range' a -> Bool

(/=) :: Range' a -> Range' a -> Bool

Ord a => Ord (Range' a)

Defined in Cornelis.Types.Agda

Methods

compare :: Range' a -> Range' a -> Ordering

(<) :: Range' a -> Range' a -> Bool

(<=) :: Range' a -> Range' a -> Bool

(>) :: Range' a -> Range' a -> Bool

(>=) :: Range' a -> Range' a -> Bool

max :: Range' a -> Range' a -> Range' a

min :: Range' a -> Range' a -> Range' a

type Rep (Range' a)

Defined in Cornelis.Types.Agda

type Rep (Range' a) = D1 ('MetaData "Range'" "Cornelis.Types.Agda" "cornelis-0.2.0.0-6a1gQdmcW6s9D29V5A3o0J" 'False) (C1 ('MetaCons "NoRange" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Range" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Seq IntervalWithoutFile))))

type SrcFile = Maybe AbsolutePath

newtype AbsolutePath

Constructors

AbsolutePath

Fields

• textPath :: String

Instances

Show AbsolutePath

Defined in Cornelis.Types.Agda

Methods

showsPrec :: Int -> AbsolutePath -> ShowS

show :: AbsolutePath -> String

showList :: [AbsolutePath] -> ShowS

Eq AbsolutePath

Defined in Cornelis.Types.Agda

Methods

(==) :: AbsolutePath -> AbsolutePath -> Bool

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

Ord AbsolutePath

Defined in Cornelis.Types.Agda

Methods

compare :: AbsolutePath -> AbsolutePath -> Ordering

(<) :: AbsolutePath -> AbsolutePath -> Bool

(<=) :: AbsolutePath -> AbsolutePath -> Bool

(>) :: AbsolutePath -> AbsolutePath -> Bool

(>=) :: AbsolutePath -> AbsolutePath -> Bool

max :: AbsolutePath -> AbsolutePath -> AbsolutePath

min :: AbsolutePath -> AbsolutePath -> AbsolutePath

type Range = Range' SrcFile

type IOTCM = IOTCM' Range

data IOTCM' range

Constructors

IOTCM Text HighlightingLevel HighlightingMethod (Interaction' range)

Instances

Foldable IOTCM'

Defined in Cornelis.Types.Agda

Methods

fold :: Monoid m => IOTCM' m -> m

foldMap :: Monoid m => (a -> m) -> IOTCM' a -> m

foldMap' :: Monoid m => (a -> m) -> IOTCM' a -> m

foldr :: (a -> b -> b) -> b -> IOTCM' a -> b

foldr' :: (a -> b -> b) -> b -> IOTCM' a -> b

foldl :: (b -> a -> b) -> b -> IOTCM' a -> b

foldl' :: (b -> a -> b) -> b -> IOTCM' a -> b

foldr1 :: (a -> a -> a) -> IOTCM' a -> a

foldl1 :: (a -> a -> a) -> IOTCM' a -> a

toList :: IOTCM' a -> [a]

null :: IOTCM' a -> Bool

length :: IOTCM' a -> Int

elem :: Eq a => a -> IOTCM' a -> Bool

maximum :: Ord a => IOTCM' a -> a

minimum :: Ord a => IOTCM' a -> a

sum :: Num a => IOTCM' a -> a

product :: Num a => IOTCM' a -> a

Traversable IOTCM'

Defined in Cornelis.Types.Agda

Methods

traverse :: Applicative f => (a -> f b) -> IOTCM' a -> f (IOTCM' b)

sequenceA :: Applicative f => IOTCM' (f a) -> f (IOTCM' a)

mapM :: Monad m => (a -> m b) -> IOTCM' a -> m (IOTCM' b)

sequence :: Monad m => IOTCM' (m a) -> m (IOTCM' a)

Functor IOTCM'

Defined in Cornelis.Types.Agda

Methods

fmap :: (a -> b) -> IOTCM' a -> IOTCM' b

(<$) :: a -> IOTCM' b -> IOTCM' a

Read range => Read (IOTCM' range)

Defined in Cornelis.Types.Agda

Methods

readsPrec :: Int -> ReadS (IOTCM' range)

readList :: ReadS [IOTCM' range]

readPrec :: ReadPrec (IOTCM' range)

readListPrec :: ReadPrec [IOTCM' range]

Show range => Show (IOTCM' range)

Defined in Cornelis.Types.Agda

Methods

showsPrec :: Int -> IOTCM' range -> ShowS

show :: IOTCM' range -> String

showList :: [IOTCM' range] -> ShowS

data Interaction' range

Constructors

Cmd_load Text [String]

cmd_load m argv loads the module in file m, using argv as the command-line options.

Cmd_constraints

Cmd_metas Rewrite

Show unsolved metas. If there are no unsolved metas but unsolved constraints show those instead.

Cmd_show_module_contents_toplevel Rewrite String

Shows all the top-level names in the given module, along with their types. Uses the top-level scope.

Cmd_search_about_toplevel Rewrite String

Shows all the top-level names in scope which mention all the given identifiers in their type.

Cmd_solveAll Rewrite

Solve (all goals / the goal at point) whose values are determined by the constraints.

Cmd_solveOne Rewrite InteractionId range String

Cmd_autoOne InteractionId range String

Solve (all goals / the goal at point) by using Auto.

Cmd_autoAll

Cmd_infer_toplevel Rewrite String

Parse the given expression (as if it were defined at the top-level of the current module) and infer its type.

Cmd_compute_toplevel ComputeMode String

Parse and type check the given expression (as if it were defined at the top-level of the current module) and normalise it.

Cmd_load_highlighting_info FilePath

cmd_load_highlighting_info source loads syntax highlighting information for the module in source, and asks Emacs to apply highlighting info from this file.

If the module does not exist, or its module name is malformed or cannot be determined, or the module has not already been visited, or the cached info is out of date, then no highlighting information is printed.

This command is used to load syntax highlighting information when a new file is opened, and it would probably be annoying if jumping to the definition of an identifier reset the proof state, so this command tries not to do that. One result of this is that the command uses the current include directories, whatever they happen to be.

Cmd_tokenHighlighting FilePath Remove

Tells Agda to compute token-based highlighting information for the file.

This command works even if the file's module name does not match its location in the file system, or if the file is not scope-correct. Furthermore no file names are put in the generated output. Thus it is fine to put source code into a temporary file before calling this command. However, the file extension should be correct.

If the second argument is Remove, then the (presumably temporary) file is removed after it has been read.

Cmd_highlight InteractionId range String

Tells Agda to compute highlighting information for the expression just spliced into an interaction point.

ShowImplicitArgs Bool

Tells Agda whether or not to show implicit arguments.

ToggleImplicitArgs

Toggle display of implicit arguments.

ShowIrrelevantArgs Bool

Tells Agda whether or not to show irrelevant arguments.

ToggleIrrelevantArgs

Toggle display of irrelevant arguments.

Cmd_give UseForce InteractionId range String

Goal commands

If the range is noRange, then the string comes from the minibuffer rather than the goal.

Cmd_refine InteractionId range String

Cmd_intro Bool InteractionId range String

Cmd_refine_or_intro Bool InteractionId range String

Cmd_context Rewrite InteractionId range String

Cmd_helper_function Rewrite InteractionId range String

Cmd_infer Rewrite InteractionId range String

Cmd_goal_type Rewrite InteractionId range String

Cmd_elaborate_give Rewrite InteractionId range String

Grabs the current goal's type and checks the expression in the hole against it. Returns the elaborated term.

Cmd_goal_type_context Rewrite InteractionId range String

Displays the current goal and context.

Cmd_goal_type_context_infer Rewrite InteractionId range String

Displays the current goal and context and infers the type of an expression.

Cmd_goal_type_context_check Rewrite InteractionId range String

Grabs the current goal's type and checks the expression in the hole against it.

Cmd_show_module_contents Rewrite InteractionId range String

Shows all the top-level names in the given module, along with their types. Uses the scope of the given goal.

Cmd_make_case InteractionId range String

Cmd_compute ComputeMode InteractionId range String

Cmd_why_in_scope InteractionId range String

Cmd_why_in_scope_toplevel String

Cmd_show_version

Displays version of the running Agda

Cmd_abort

Abort the current computation.

Does nothing if no computation is in progress.

Cmd_exit

Exit the program.

Instances

Foldable Interaction'

Defined in Cornelis.Types.Agda

Methods

fold :: Monoid m => Interaction' m -> m

foldMap :: Monoid m => (a -> m) -> Interaction' a -> m

foldMap' :: Monoid m => (a -> m) -> Interaction' a -> m

foldr :: (a -> b -> b) -> b -> Interaction' a -> b

foldr' :: (a -> b -> b) -> b -> Interaction' a -> b

foldl :: (b -> a -> b) -> b -> Interaction' a -> b

foldl' :: (b -> a -> b) -> b -> Interaction' a -> b

foldr1 :: (a -> a -> a) -> Interaction' a -> a

foldl1 :: (a -> a -> a) -> Interaction' a -> a

toList :: Interaction' a -> [a]

null :: Interaction' a -> Bool

length :: Interaction' a -> Int

elem :: Eq a => a -> Interaction' a -> Bool

maximum :: Ord a => Interaction' a -> a

minimum :: Ord a => Interaction' a -> a

sum :: Num a => Interaction' a -> a

product :: Num a => Interaction' a -> a

Traversable Interaction'

Defined in Cornelis.Types.Agda

Methods

traverse :: Applicative f => (a -> f b) -> Interaction' a -> f (Interaction' b)

sequenceA :: Applicative f => Interaction' (f a) -> f (Interaction' a)

mapM :: Monad m => (a -> m b) -> Interaction' a -> m (Interaction' b)

sequence :: Monad m => Interaction' (m a) -> m (Interaction' a)

Functor Interaction'

Defined in Cornelis.Types.Agda

Methods

fmap :: (a -> b) -> Interaction' a -> Interaction' b

(<$) :: a -> Interaction' b -> Interaction' a

Read range => Read (Interaction' range)

Defined in Cornelis.Types.Agda

Methods

readsPrec :: Int -> ReadS (Interaction' range)

readList :: ReadS [Interaction' range]

readPrec :: ReadPrec (Interaction' range)

readListPrec :: ReadPrec [Interaction' range]

Show range => Show (Interaction' range)

Defined in Cornelis.Types.Agda

Methods

showsPrec :: Int -> Interaction' range -> ShowS

show :: Interaction' range -> String

showList :: [Interaction' range] -> ShowS

type Interaction = Interaction' Range

data HighlightingLevel

Constructors

None

NonInteractive

Interactive

This includes both non-interactive highlighting and interactive highlighting of the expression that is currently being type-checked.

Instances

Generic HighlightingLevel

Defined in Cornelis.Types.Agda

Associated Types

type Rep HighlightingLevel :: Type -> Type

Methods

from :: HighlightingLevel -> Rep HighlightingLevel x

to :: Rep HighlightingLevel x -> HighlightingLevel

Read HighlightingLevel

Defined in Cornelis.Types.Agda

Methods

readsPrec :: Int -> ReadS HighlightingLevel

readList :: ReadS [HighlightingLevel]

readPrec :: ReadPrec HighlightingLevel

readListPrec :: ReadPrec [HighlightingLevel]

Show HighlightingLevel

Defined in Cornelis.Types.Agda

Methods

showsPrec :: Int -> HighlightingLevel -> ShowS

show :: HighlightingLevel -> String

showList :: [HighlightingLevel] -> ShowS

Eq HighlightingLevel

Defined in Cornelis.Types.Agda

Methods

(==) :: HighlightingLevel -> HighlightingLevel -> Bool

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

Ord HighlightingLevel

Defined in Cornelis.Types.Agda

Methods

compare :: HighlightingLevel -> HighlightingLevel -> Ordering

(<) :: HighlightingLevel -> HighlightingLevel -> Bool

(<=) :: HighlightingLevel -> HighlightingLevel -> Bool

(>) :: HighlightingLevel -> HighlightingLevel -> Bool

(>=) :: HighlightingLevel -> HighlightingLevel -> Bool

max :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel

min :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel

type Rep HighlightingLevel

Defined in Cornelis.Types.Agda

type Rep HighlightingLevel = D1 ('MetaData "HighlightingLevel" "Cornelis.Types.Agda" "cornelis-0.2.0.0-6a1gQdmcW6s9D29V5A3o0J" 'False) (C1 ('MetaCons "None" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NonInteractive" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Interactive" 'PrefixI 'False) (U1 :: Type -> Type)))

data HighlightingMethod

Constructors

Direct

Via stdout.

Indirect

Both via files and via stdout.

Instances

Generic HighlightingMethod

Defined in Cornelis.Types.Agda

Associated Types

type Rep HighlightingMethod :: Type -> Type

Methods

from :: HighlightingMethod -> Rep HighlightingMethod x

to :: Rep HighlightingMethod x -> HighlightingMethod

Read HighlightingMethod

Defined in Cornelis.Types.Agda

Methods

readsPrec :: Int -> ReadS HighlightingMethod

readList :: ReadS [HighlightingMethod]

readPrec :: ReadPrec HighlightingMethod

readListPrec :: ReadPrec [HighlightingMethod]

Show HighlightingMethod

Defined in Cornelis.Types.Agda

Methods

showsPrec :: Int -> HighlightingMethod -> ShowS

show :: HighlightingMethod -> String

showList :: [HighlightingMethod] -> ShowS

Eq HighlightingMethod

Defined in Cornelis.Types.Agda

Methods

(==) :: HighlightingMethod -> HighlightingMethod -> Bool

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

type Rep HighlightingMethod

Defined in Cornelis.Types.Agda

type Rep HighlightingMethod = D1 ('MetaData "HighlightingMethod" "Cornelis.Types.Agda" "cornelis-0.2.0.0-6a1gQdmcW6s9D29V5A3o0J" 'False) (C1 ('MetaCons "Direct" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Indirect" 'PrefixI 'False) (U1 :: Type -> Type))

data Remove

Constructors

Remove

Keep

Instances

Read Remove

Defined in Cornelis.Types.Agda

Methods

readsPrec :: Int -> ReadS Remove

readList :: ReadS [Remove]

readPrec :: ReadPrec Remove

readListPrec :: ReadPrec [Remove]

Show Remove

Defined in Cornelis.Types.Agda

Methods

showsPrec :: Int -> Remove -> ShowS

show :: Remove -> String

showList :: [Remove] -> ShowS

noRange :: Range' a

intervalToRange :: a -> IntervalWithoutFile -> Range' a

Converts a file name and an interval to a range.

intervalsToRange :: a -> [IntervalWithoutFile] -> Range' a

Turns a file name plus a list of intervals into a range.

Precondition: consecutiveAndSeparated.

mkAbsPathRnage :: Text -> IntervalWithoutFile -> Range