Mikan
Safe HaskellNone
LanguageHaskell2010

Mikan.TypeChecking.Monad.Base.Types

Description

Data structures for the type checker.

Part of Agda.TypeChecking.Monad.Base, extracted to avoid import cycles.

Synopsis

Documentation

pattern CxEmpty :: Context Source #

pattern CxExtend :: ContextEntry -> Context -> Context Source #

pattern CxExtendVar :: Name -> Dom Type -> Context -> Context Source #

cxDrop :: Nat -> Context -> Context Source #

cxLookup :: Nat -> Context -> Maybe ContextEntry Source #

Does not raise the retrieved entry!

cxPrepend :: [ContextEntry] -> Context -> Context Source #

Assumes the list of entries to be prepended follows the context ordering convention (earlier entries depend on later ones)

cxSplitAt :: Nat -> Context -> ([ContextEntry], Context) Source #

The returned prefix follows the context ordering convention (earlier entries depend on later ones)

cxTake :: Nat -> Context -> [ContextEntry] Source #

The returned list of context entries follows the context ordering convention (earlier entries depend on later ones)

cxWithIndex :: (Nat -> ContextEntry -> a) -> Context -> [a] Source #

lensFileDictBuiltinModuleIds :: Lens' FileDictWithBuiltins BuiltinModuleIds Source #

lensFileDictFileDictBuilder :: Lens' FileDictWithBuiltins FileDictBuilder Source #

lensFileDictPrimitiveLibDir :: Lens' FileDictWithBuiltins PrimitiveLibDir Source #

lensPairModuleToSource :: Lens' (FileDictWithBuiltins, ModuleToSourceId) ModuleToSource Source #

type BuiltinModuleIds = EnumMap FileId IsBuiltinModule Source #

Collection of FileIds of primitive modules.

data Comparison Source #

Constructors

CmpEq 
CmpLeq 

Instances

Instances details
Pretty Comparison Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base

Methods

pretty :: Comparison -> Doc Source #

prettyPrec :: Int -> Comparison -> Doc Source #

prettyList :: [Comparison] -> Doc Source #

PrettyTCM Comparison Source # 
Instance details

Defined in Mikan.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Comparison -> m Doc Source #

EmbPrj Comparison Source # 
Instance details

Defined in Mikan.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Comparison -> S Word32 Source #

icod_ :: Comparison -> S Word32 Source #

value :: Word32 -> R Comparison Source #

NFData Comparison Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base

Methods

rnf :: Comparison -> () #

Generic Comparison Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Associated Types

type Rep Comparison 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep Comparison = D1 ('MetaData "Comparison" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "CmpEq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CmpLeq" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: Comparison -> Rep Comparison x #

to :: Rep Comparison x -> Comparison #

Show Comparison Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

showsPrec :: Int -> Comparison -> ShowS #

show :: Comparison -> String #

showList :: [Comparison] -> ShowS #

Eq Comparison Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

(==) :: Comparison -> Comparison -> Bool #

(/=) :: Comparison -> Comparison -> Bool #

type Rep Comparison Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep Comparison = D1 ('MetaData "Comparison" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "CmpEq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CmpLeq" 'PrefixI 'False) (U1 :: Type -> Type))

type Context = Context' ContextEntry Source #

newtype Context' a Source #

The Context is a stack of ContextEntrys. Unlike telescopes, later context entries are bound in earlier ones.

Constructors

Context 

Fields

Instances

Instances details
Reify Context Source # 
Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Context 
Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

type ReifiesTo Context = [TypedBinding]

Methods

reify :: MonadReify m => Context -> m (ReifiesTo Context) Source #

reifyWhen :: MonadReify m => Bool -> Context -> m (ReifiesTo Context) Source #

AddContext Context Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Context -> m a -> m a Source #

PrettyTCM Context Source # 
Instance details

Defined in Mikan.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Context -> m Doc Source #

InstantiateFull Context Source # 
Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

instantiateFull' :: Context -> ReduceM Context Source #

EmbPrj Context Source # 
Instance details

Defined in Mikan.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Context -> S Word32 Source #

icod_ :: Context -> S Word32 Source #

value :: Word32 -> R Context Source #

NFData Context Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

rnf :: Context -> () #

Functor Context' Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

fmap :: (a -> b) -> Context' a -> Context' b #

(<$) :: a -> Context' b -> Context' a #

Foldable Context' Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

fold :: Monoid m => Context' m -> m #

foldMap :: Monoid m => (a -> m) -> Context' a -> m #

foldMap' :: Monoid m => (a -> m) -> Context' a -> m #

foldr :: (a -> b -> b) -> b -> Context' a -> b #

foldr' :: (a -> b -> b) -> b -> Context' a -> b #

foldl :: (b -> a -> b) -> b -> Context' a -> b #

foldl' :: (b -> a -> b) -> b -> Context' a -> b #

foldr1 :: (a -> a -> a) -> Context' a -> a #

foldl1 :: (a -> a -> a) -> Context' a -> a #

toList :: Context' a -> [a] #

null :: Context' a -> Bool #

length :: Context' a -> Int #

elem :: Eq a => a -> Context' a -> Bool #

maximum :: Ord a => Context' a -> a #

minimum :: Ord a => Context' a -> a #

sum :: Num a => Context' a -> a #

product :: Num a => Context' a -> a #

Traversable Context' Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

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

sequenceA :: Applicative f => Context' (f a) -> f (Context' a) #

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

sequence :: Monad m => Context' (m a) -> m (Context' a) #

Null (Context' a) Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

empty :: Context' a Source #

null :: Context' a -> Bool Source #

Sized (Context' a) Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

size :: Context' a -> Int Source #

natSize :: Context' a -> Peano Source #

Generic (Context' a) Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Associated Types

type Rep (Context' a) 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep (Context' a) = D1 ('MetaData "Context'" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'True) (C1 ('MetaCons "Context" 'PrefixI 'True) (S1 ('MetaSel ('Just "cxEntries") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [a])))

Methods

from :: Context' a -> Rep (Context' a) x #

to :: Rep (Context' a) x -> Context' a #

Show a => Show (Context' a) Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

showsPrec :: Int -> Context' a -> ShowS #

show :: Context' a -> String #

showList :: [Context' a] -> ShowS #

type ReifiesTo Context Source # 
Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

type ReifiesTo Context = [TypedBinding]
type Rep (Context' a) Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep (Context' a) = D1 ('MetaData "Context'" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'True) (C1 ('MetaCons "Context" 'PrefixI 'True) (S1 ('MetaSel ('Just "cxEntries") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [a])))

data ContextEntry Source #

Constructors

CtxVar 

Fields

Instances

Instances details
LensArgInfo ContextEntry Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

getArgInfo :: ContextEntry -> ArgInfo Source #

setArgInfo :: ArgInfo -> ContextEntry -> ContextEntry Source #

mapArgInfo :: (ArgInfo -> ArgInfo) -> ContextEntry -> ContextEntry Source #

LensHiding ContextEntry Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

getHiding :: ContextEntry -> Hiding Source #

setHiding :: Hiding -> ContextEntry -> ContextEntry Source #

mapHiding :: (Hiding -> Hiding) -> ContextEntry -> ContextEntry Source #

LensOrigin ContextEntry Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

getOrigin :: ContextEntry -> Origin Source #

setOrigin :: Origin -> ContextEntry -> ContextEntry Source #

mapOrigin :: (Origin -> Origin) -> ContextEntry -> ContextEntry Source #

Reify Context Source # 
Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Context 
Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

type ReifiesTo Context = [TypedBinding]

Methods

reify :: MonadReify m => Context -> m (ReifiesTo Context) Source #

reifyWhen :: MonadReify m => Bool -> Context -> m (ReifiesTo Context) Source #

Reify ContextEntry Source # 
Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo ContextEntry 
Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

type ReifiesTo ContextEntry = TypedBinding

Methods

reify :: MonadReify m => ContextEntry -> m (ReifiesTo ContextEntry) Source #

reifyWhen :: MonadReify m => Bool -> ContextEntry -> m (ReifiesTo ContextEntry) Source #

AddContext Context Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Context -> m a -> m a Source #

AddContext ContextEntry Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ContextEntry -> m a -> m a Source #

PrettyTCM Context Source # 
Instance details

Defined in Mikan.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Context -> m Doc Source #

PrettyTCM ContextEntry Source # 
Instance details

Defined in Mikan.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => ContextEntry -> m Doc Source #

InstantiateFull Context Source # 
Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

instantiateFull' :: Context -> ReduceM Context Source #

InstantiateFull ContextEntry Source # 
Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

instantiateFull' :: ContextEntry -> ReduceM ContextEntry Source #

EmbPrj Context Source # 
Instance details

Defined in Mikan.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Context -> S Word32 Source #

icod_ :: Context -> S Word32 Source #

value :: Word32 -> R Context Source #

EmbPrj ContextEntry Source # 
Instance details

Defined in Mikan.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ContextEntry -> S Word32 Source #

icod_ :: ContextEntry -> S Word32 Source #

value :: Word32 -> R ContextEntry Source #

Subst ContextEntry Source # 
Instance details

Defined in Mikan.TypeChecking.Substitute

Associated Types

type SubstArg ContextEntry 
Instance details

Defined in Mikan.TypeChecking.Substitute

type SubstArg ContextEntry = Term

Methods

applySubst :: Substitution' (SubstArg ContextEntry) -> ContextEntry -> ContextEntry Source #

NFData Context Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

rnf :: Context -> () #

NFData ContextEntry Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

rnf :: ContextEntry -> () #

Generic ContextEntry Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Associated Types

type Rep ContextEntry 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep ContextEntry = D1 ('MetaData "ContextEntry" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "CtxVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "ceName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "ceType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type))))

Methods

from :: ContextEntry -> Rep ContextEntry x #

to :: Rep ContextEntry x -> ContextEntry #

Show ContextEntry Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

showsPrec :: Int -> ContextEntry -> ShowS #

show :: ContextEntry -> String #

showList :: [ContextEntry] -> ShowS #

type ReifiesTo Context Source # 
Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

type ReifiesTo Context = [TypedBinding]
type ReifiesTo ContextEntry Source # 
Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

type ReifiesTo ContextEntry = TypedBinding
type SubstArg ContextEntry Source # 
Instance details

Defined in Mikan.TypeChecking.Substitute

type SubstArg ContextEntry = Term
type Rep ContextEntry Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep ContextEntry = D1 ('MetaData "ContextEntry" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "CtxVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "ceName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "ceType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type))))

data FileDictWithBuiltins Source #

Translation between AbsolutePath and FileId that also knows about Agda's builtin modules.

Constructors

FileDictWithBuiltins 

Fields

Instances

Instances details
GetFileId FileDictWithBuiltins Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base

Methods

getFileId :: FileDictWithBuiltins -> File -> FileId Source #

GetIdFile FileDictWithBuiltins Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base

Methods

getIdFile :: FileDictWithBuiltins -> FileId -> File Source #

NFData FileDictWithBuiltins Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

rnf :: FileDictWithBuiltins -> () #

Generic FileDictWithBuiltins Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Associated Types

type Rep FileDictWithBuiltins 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep FileDictWithBuiltins = D1 ('MetaData "FileDictWithBuiltins" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "FileDictWithBuiltins" 'PrefixI 'True) (S1 ('MetaSel ('Just "fileDictBuilder") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FileDictBuilder) :*: (S1 ('MetaSel ('Just "builtinModuleIds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 BuiltinModuleIds) :*: S1 ('MetaSel ('Just "primitiveLibDir") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 PrimitiveLibDir))))

Methods

from :: FileDictWithBuiltins -> Rep FileDictWithBuiltins x #

to :: Rep FileDictWithBuiltins x -> FileDictWithBuiltins #

type Rep FileDictWithBuiltins Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep FileDictWithBuiltins = D1 ('MetaData "FileDictWithBuiltins" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "FileDictWithBuiltins" 'PrefixI 'True) (S1 ('MetaSel ('Just "fileDictBuilder") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FileDictBuilder) :*: (S1 ('MetaSel ('Just "builtinModuleIds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 BuiltinModuleIds) :*: S1 ('MetaSel ('Just "primitiveLibDir") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 PrimitiveLibDir))))

data HighlightingLevel Source #

How much highlighting should be sent to the user interface?

Constructors

None 
NonInteractive 
Interactive

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

Instances

Instances details
NFData HighlightingLevel Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base

Methods

rnf :: HighlightingLevel -> () #

Generic HighlightingLevel Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Associated Types

type Rep HighlightingLevel 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep HighlightingLevel = D1 ('MetaData "HighlightingLevel" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" '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)))

Methods

from :: HighlightingLevel -> Rep HighlightingLevel x #

to :: Rep HighlightingLevel x -> HighlightingLevel #

Read HighlightingLevel Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

readsPrec :: Int -> ReadS HighlightingLevel #

readList :: ReadS [HighlightingLevel] #

readPrec :: ReadPrec HighlightingLevel #

readListPrec :: ReadPrec [HighlightingLevel] #

Show HighlightingLevel Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

showsPrec :: Int -> HighlightingLevel -> ShowS #

show :: HighlightingLevel -> String #

showList :: [HighlightingLevel] -> ShowS #

Eq HighlightingLevel Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

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

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

Ord HighlightingLevel Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

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 Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep HighlightingLevel = D1 ('MetaData "HighlightingLevel" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" '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 Source #

How should highlighting be sent to the user interface?

Constructors

Direct

Via stdout.

Indirect

Both via files and via stdout.

Instances

Instances details
NFData HighlightingMethod Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base

Methods

rnf :: HighlightingMethod -> () #

Generic HighlightingMethod Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Associated Types

type Rep HighlightingMethod 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep HighlightingMethod = D1 ('MetaData "HighlightingMethod" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "Direct" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Indirect" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: HighlightingMethod -> Rep HighlightingMethod x #

to :: Rep HighlightingMethod x -> HighlightingMethod #

Read HighlightingMethod Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

readsPrec :: Int -> ReadS HighlightingMethod #

readList :: ReadS [HighlightingMethod] #

readPrec :: ReadPrec HighlightingMethod #

readListPrec :: ReadPrec [HighlightingMethod] #

Show HighlightingMethod Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

showsPrec :: Int -> HighlightingMethod -> ShowS #

show :: HighlightingMethod -> String #

showList :: [HighlightingMethod] -> ShowS #

Eq HighlightingMethod Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

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

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

type Rep HighlightingMethod Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep HighlightingMethod = D1 ('MetaData "HighlightingMethod" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "Direct" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Indirect" 'PrefixI 'False) (U1 :: Type -> Type))

data IPFace' t Source #

Datatype representing a single boundary condition: x_0 = u_0, ... ,x_n = u_n ⊢ t = ?n es

Constructors

IPFace' 

Fields

Instances

Instances details
Pretty c => Pretty (IPFace' c) Source # 
Instance details

Defined in Mikan.Interaction.BasicOps

Methods

pretty :: IPFace' c -> Doc Source #

prettyPrec :: Int -> IPFace' c -> Doc Source #

prettyList :: [IPFace' c] -> Doc Source #

data IsBuiltinModule Source #

Discern Agda's primitive modules from other file modules. @IsPrimitiveModule implies IsBuiltinModuleWithSafePostulate implies isBuiltinModule.

Constructors

IsPrimitiveModule

Very magical module, e.g. Agda.Primitive.

IsBuiltinModuleWithSafePostulates

Safe module, e.g. Agda.Builtin.Equality.

IsBuiltinModule

Any builtin module.

Instances

Instances details
NFData IsBuiltinModule Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

rnf :: IsBuiltinModule -> () #

Generic IsBuiltinModule Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Associated Types

type Rep IsBuiltinModule 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep IsBuiltinModule = D1 ('MetaData "IsBuiltinModule" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "IsPrimitiveModule" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "IsBuiltinModuleWithSafePostulates" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsBuiltinModule" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: IsBuiltinModule -> Rep IsBuiltinModule x #

to :: Rep IsBuiltinModule x -> IsBuiltinModule #

Show IsBuiltinModule Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

showsPrec :: Int -> IsBuiltinModule -> ShowS #

show :: IsBuiltinModule -> String #

showList :: [IsBuiltinModule] -> ShowS #

Eq IsBuiltinModule Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

(==) :: IsBuiltinModule -> IsBuiltinModule -> Bool #

(/=) :: IsBuiltinModule -> IsBuiltinModule -> Bool #

Ord IsBuiltinModule Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

compare :: IsBuiltinModule -> IsBuiltinModule -> Ordering #

(<) :: IsBuiltinModule -> IsBuiltinModule -> Bool #

(<=) :: IsBuiltinModule -> IsBuiltinModule -> Bool #

(>) :: IsBuiltinModule -> IsBuiltinModule -> Bool #

(>=) :: IsBuiltinModule -> IsBuiltinModule -> Bool #

max :: IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule #

min :: IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule #

type Rep IsBuiltinModule Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep IsBuiltinModule = D1 ('MetaData "IsBuiltinModule" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "IsPrimitiveModule" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "IsBuiltinModuleWithSafePostulates" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsBuiltinModule" 'PrefixI 'False) (U1 :: Type -> Type)))

data ModuleToSource Source #

Constructors

ModuleToSource 

Fields

Instances

Instances details
Pretty ModuleToSource Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base

Methods

pretty :: ModuleToSource -> Doc Source #

prettyPrec :: Int -> ModuleToSource -> Doc Source #

prettyList :: [ModuleToSource] -> Doc Source #

type ModuleToSourceId = Map TopLevelModuleName SourceFile Source #

Maps top-level module names to the corresponding source file ids.

data NamedMeta Source #

For printing, we couple a meta with its name suggestion.

Constructors

NamedMeta 

Fields

Instances

Instances details
EncodeTCM NamedMeta Source # 
Instance details

Defined in Mikan.Interaction.JSONTop

Methods

encodeTCM :: NamedMeta -> TCM Value Source #

Pretty NamedMeta Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base

Methods

pretty :: NamedMeta -> Doc Source #

prettyPrec :: Int -> NamedMeta -> Doc Source #

prettyList :: [NamedMeta] -> Doc Source #

ToConcrete NamedMeta Source # 
Instance details

Defined in Mikan.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs NamedMeta 
Instance details

Defined in Mikan.Syntax.Translation.AbstractToConcrete

type ConOfAbs NamedMeta = Expr

Methods

toConcrete :: MonadToConcrete m => NamedMeta -> m (ConOfAbs NamedMeta) Source #

bindToConcrete :: MonadToConcrete m => NamedMeta -> (ConOfAbs NamedMeta -> m b) -> m b Source #

PrettyTCM NamedMeta Source # 
Instance details

Defined in Mikan.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => NamedMeta -> m Doc Source #

type ConOfAbs NamedMeta Source # 
Instance details

Defined in Mikan.Syntax.Translation.AbstractToConcrete

type ConOfAbs NamedMeta = Expr

data Polarity Source #

Polarity for equality and subtype checking.

Constructors

Covariant

monotone

Contravariant

antitone

Invariant

no information (mixed variance)

Nonvariant

constant

Instances

Instances details
Pretty Polarity Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base

Methods

pretty :: Polarity -> Doc Source #

prettyPrec :: Int -> Polarity -> Doc Source #

prettyList :: [Polarity] -> Doc Source #

KillRange Polarity Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Polarity Source #

PrettyTCM Polarity Source # 
Instance details

Defined in Mikan.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Polarity -> m Doc Source #

EmbPrj Polarity Source # 
Instance details

Defined in Mikan.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Polarity -> S Word32 Source #

icod_ :: Polarity -> S Word32 Source #

value :: Word32 -> R Polarity Source #

NFData Polarity Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base

Methods

rnf :: Polarity -> () #

Generic Polarity Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Associated Types

type Rep Polarity 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep Polarity = D1 ('MetaData "Polarity" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) ((C1 ('MetaCons "Covariant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Contravariant" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Invariant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Nonvariant" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: Polarity -> Rep Polarity x #

to :: Rep Polarity x -> Polarity #

Show Polarity Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

showsPrec :: Int -> Polarity -> ShowS #

show :: Polarity -> String #

showList :: [Polarity] -> ShowS #

Eq Polarity Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

(==) :: Polarity -> Polarity -> Bool #

(/=) :: Polarity -> Polarity -> Bool #

Abstract [Polarity] Source # 
Instance details

Defined in Mikan.TypeChecking.Substitute

Methods

abstract :: Telescope -> [Polarity] -> [Polarity] Source #

Apply [Polarity] Source # 
Instance details

Defined in Mikan.TypeChecking.Substitute

Methods

apply :: [Polarity] -> Args -> [Polarity] Source #

applyE :: [Polarity] -> Elims -> [Polarity] Source #

type Rep Polarity Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep Polarity = D1 ('MetaData "Polarity" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) ((C1 ('MetaCons "Covariant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Contravariant" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Invariant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Nonvariant" 'PrefixI 'False) (U1 :: Type -> Type)))

type PrimitiveLibDir = AbsolutePath Source #

newtype SourceFile Source #

SourceFiles must exist and be registered in our file dictionary.

Constructors

SourceFile 

Fields

Instances

Instances details
NFData SourceFile Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

rnf :: SourceFile -> () #

Generic SourceFile Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Associated Types

type Rep SourceFile 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep SourceFile = D1 ('MetaData "SourceFile" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'True) (C1 ('MetaCons "SourceFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "srcFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId)))

Methods

from :: SourceFile -> Rep SourceFile x #

to :: Rep SourceFile x -> SourceFile #

Show SourceFile Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

showsPrec :: Int -> SourceFile -> ShowS #

show :: SourceFile -> String #

showList :: [SourceFile] -> ShowS #

Eq SourceFile Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

(==) :: SourceFile -> SourceFile -> Bool #

(/=) :: SourceFile -> SourceFile -> Bool #

Ord SourceFile Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

compare :: SourceFile -> SourceFile -> Ordering #

(<) :: SourceFile -> SourceFile -> Bool #

(<=) :: SourceFile -> SourceFile -> Bool #

(>) :: SourceFile -> SourceFile -> Bool #

(>=) :: SourceFile -> SourceFile -> Bool #

max :: SourceFile -> SourceFile -> SourceFile #

min :: SourceFile -> SourceFile -> SourceFile #

type Rep SourceFile Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep SourceFile = D1 ('MetaData "SourceFile" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'True) (C1 ('MetaCons "SourceFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "srcFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId)))

data TopLevelModuleNameWithSourceFile Source #

Constructors

TopLevelModuleNameWithSourceFile 

Fields

Instances

Instances details
PrettyTCM TopLevelModuleNameWithSourceFile Source # 
Instance details

Defined in Mikan.TypeChecking.Errors

Methods

prettyTCM :: MonadPretty m => TopLevelModuleNameWithSourceFile -> m Doc Source #

NFData TopLevelModuleNameWithSourceFile Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

rnf :: TopLevelModuleNameWithSourceFile -> () #

Generic TopLevelModuleNameWithSourceFile Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Associated Types

type Rep TopLevelModuleNameWithSourceFile 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep TopLevelModuleNameWithSourceFile = D1 ('MetaData "TopLevelModuleNameWithSourceFile" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "TopLevelModuleNameWithSourceFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "fileModuleName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleName) :*: S1 ('MetaSel ('Just "fileModuleSourceFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SourceFile)))

Methods

from :: TopLevelModuleNameWithSourceFile -> Rep TopLevelModuleNameWithSourceFile x #

to :: Rep TopLevelModuleNameWithSourceFile x -> TopLevelModuleNameWithSourceFile #

Show TopLevelModuleNameWithSourceFile Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

Methods

showsPrec :: Int -> TopLevelModuleNameWithSourceFile -> ShowS #

show :: TopLevelModuleNameWithSourceFile -> String #

showList :: [TopLevelModuleNameWithSourceFile] -> ShowS #

type Rep TopLevelModuleNameWithSourceFile Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Base.Types

type Rep TopLevelModuleNameWithSourceFile = D1 ('MetaData "TopLevelModuleNameWithSourceFile" "Mikan.TypeChecking.Monad.Base.Types" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "TopLevelModuleNameWithSourceFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "fileModuleName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleName) :*: S1 ('MetaSel ('Just "fileModuleSourceFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SourceFile)))

type TopLevelModuleName = TopLevelModuleName' Range Source #

Top-level module names (with constant-time comparisons).

data FileDictBuilder Source #

Instances

Instances details
GetFileId FileDictBuilder Source # 
Instance details

Defined in Mikan.Utils.FileId

Methods

getFileId :: FileDictBuilder -> File -> FileId Source #

GetIdFile FileDictBuilder Source # 
Instance details

Defined in Mikan.Utils.FileId

Methods

getIdFile :: FileDictBuilder -> FileId -> File Source #

Null FileDictBuilder Source # 
Instance details

Defined in Mikan.Utils.FileId

Methods

empty :: FileDictBuilder Source #

null :: FileDictBuilder -> Bool Source #

NFData FileDictBuilder Source # 
Instance details

Defined in Mikan.Utils.FileId

Methods

rnf :: FileDictBuilder -> () #

Generic FileDictBuilder Source # 
Instance details

Defined in Mikan.Utils.FileId

Associated Types

type Rep FileDictBuilder 
Instance details

Defined in Mikan.Utils.FileId

type Rep FileDictBuilder = D1 ('MetaData "FileDictBuilder" "Mikan.Utils.FileId" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "FileDictBuilder" 'PrefixI 'True) (S1 ('MetaSel ('Just "nextFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId) :*: S1 ('MetaSel ('Just "fileDict") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileDict)))

Methods

from :: FileDictBuilder -> Rep FileDictBuilder x #

to :: Rep FileDictBuilder x -> FileDictBuilder #

type Rep FileDictBuilder Source # 
Instance details

Defined in Mikan.Utils.FileId

type Rep FileDictBuilder = D1 ('MetaData "FileDictBuilder" "Mikan.Utils.FileId" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "FileDictBuilder" 'PrefixI 'True) (S1 ('MetaSel ('Just "nextFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId) :*: S1 ('MetaSel ('Just "fileDict") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileDict)))

data FileId Source #

Unique identifier of a file.

Instances

Instances details
GetFileId FileToId Source # 
Instance details

Defined in Mikan.Utils.FileId

Methods

getFileId :: FileToId -> File -> FileId Source #

GetIdFile IdToFile Source # 
Instance details

Defined in Mikan.Utils.FileId

Methods

getIdFile :: IdToFile -> FileId -> File Source #

NFData FileId Source # 
Instance details

Defined in Mikan.Utils.FileId

Methods

rnf :: FileId -> () #

Enum FileId Source # 
Instance details

Defined in Mikan.Utils.FileId

Methods

succ :: FileId -> FileId #

pred :: FileId -> FileId #

toEnum :: Int -> FileId #

fromEnum :: FileId -> Int #

enumFrom :: FileId -> [FileId] #

enumFromThen :: FileId -> FileId -> [FileId] #

enumFromTo :: FileId -> FileId -> [FileId] #

enumFromThenTo :: FileId -> FileId -> FileId -> [FileId] #

Generic FileId Source # 
Instance details

Defined in Mikan.Utils.FileId

Associated Types

type Rep FileId 
Instance details

Defined in Mikan.Utils.FileId

type Rep FileId = D1 ('MetaData "FileId" "Mikan.Utils.FileId" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'True) (C1 ('MetaCons "FileId" 'PrefixI 'True) (S1 ('MetaSel ('Just "theFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word32)))

Methods

from :: FileId -> Rep FileId x #

to :: Rep FileId x -> FileId #

Num FileId Source # 
Instance details

Defined in Mikan.Utils.FileId

Methods

(+) :: FileId -> FileId -> FileId #

(-) :: FileId -> FileId -> FileId #

(*) :: FileId -> FileId -> FileId #

negate :: FileId -> FileId #

abs :: FileId -> FileId #

signum :: FileId -> FileId #

fromInteger :: Integer -> FileId #

Show FileId Source # 
Instance details

Defined in Mikan.Utils.FileId

Methods

showsPrec :: Int -> FileId -> ShowS #

show :: FileId -> String #

showList :: [FileId] -> ShowS #

Eq FileId Source # 
Instance details

Defined in Mikan.Utils.FileId

Methods

(==) :: FileId -> FileId -> Bool #

(/=) :: FileId -> FileId -> Bool #

Ord FileId Source # 
Instance details

Defined in Mikan.Utils.FileId

Methods

compare :: FileId -> FileId -> Ordering #

(<) :: FileId -> FileId -> Bool #

(<=) :: FileId -> FileId -> Bool #

(>) :: FileId -> FileId -> Bool #

(>=) :: FileId -> FileId -> Bool #

max :: FileId -> FileId -> FileId #

min :: FileId -> FileId -> FileId #

type Rep FileId Source # 
Instance details

Defined in Mikan.Utils.FileId

type Rep FileId = D1 ('MetaData "FileId" "Mikan.Utils.FileId" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'True) (C1 ('MetaCons "FileId" 'PrefixI 'True) (S1 ('MetaSel ('Just "theFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word32)))

data AbsolutePath Source #

Paths which are known to be absolute.

Note that the Eq and Ord instances do not check if different paths point to the same files or directories.

Instances

Instances details
Pretty AbsolutePath Source # 
Instance details

Defined in Mikan.Syntax.Common.Pretty

Methods

pretty :: AbsolutePath -> Doc Source #

prettyPrec :: Int -> AbsolutePath -> Doc Source #

prettyList :: [AbsolutePath] -> Doc Source #

GetFileId FileToId Source # 
Instance details

Defined in Mikan.Utils.FileId

Methods

getFileId :: FileToId -> File -> FileId Source #

GetIdFile IdToFile Source # 
Instance details

Defined in Mikan.Utils.FileId

Methods

getIdFile :: IdToFile -> FileId -> File Source #

Null AbsolutePath Source # 
Instance details

Defined in Mikan.Utils.FileName

Methods

empty :: AbsolutePath Source #

null :: AbsolutePath -> Bool Source #

ToJSON AbsolutePath Source # 
Instance details

Defined in Mikan.Interaction.JSON

Methods

toJSON :: AbsolutePath -> Value #

toEncoding :: AbsolutePath -> Encoding #

toJSONList :: [AbsolutePath] -> Value #

toEncodingList :: [AbsolutePath] -> Encoding #

omitField :: AbsolutePath -> Bool #

NFData AbsolutePath Source # 
Instance details

Defined in Mikan.Utils.FileName

Methods

rnf :: AbsolutePath -> () #

Read AbsolutePath Source # 
Instance details

Defined in Mikan.Interaction.Base

Methods

readsPrec :: Int -> ReadS AbsolutePath #

readList :: ReadS [AbsolutePath] #

readPrec :: ReadPrec AbsolutePath #

readListPrec :: ReadPrec [AbsolutePath] #

Show AbsolutePath Source # 
Instance details

Defined in Mikan.Utils.FileName

Methods

showsPrec :: Int -> AbsolutePath -> ShowS #

show :: AbsolutePath -> String #

showList :: [AbsolutePath] -> ShowS #

Eq AbsolutePath Source # 
Instance details

Defined in Mikan.Utils.FileName

Methods

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

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

Ord AbsolutePath Source # 
Instance details

Defined in Mikan.Utils.FileName

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 #

Hashable AbsolutePath Source # 
Instance details

Defined in Mikan.Utils.FileName

Methods

hashWithSalt :: Int -> AbsolutePath -> Int #

hash :: AbsolutePath -> Int #