Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Intermediate Representation for Agda's types
Synopsis
- class FromAgda a b | a -> b where
- fromAgda :: a -> b
- class FromAgdaTCM a b | a -> b where
- fromAgdaTCM :: a -> TCM b
- data Response
- = ResponseHighlightingInfoDirect HighlightingInfos
- | ResponseHighlightingInfoIndirect FilePath
- | ResponseDisplayInfo DisplayInfo
- | ResponseStatus Bool Bool
- | ResponseClearHighlightingTokenBased
- | ResponseClearHighlightingNotOnlyTokenBased
- | ResponseRunningInfo Int String
- | ResponseClearRunningInfo
- | ResponseDoneAborting
- | ResponseDoneExiting
- | ResponseGiveAction Int GiveResult
- | ResponseInteractionPoints [Int]
- | ResponseMakeCaseFunction [String]
- | ResponseMakeCaseExtendedLambda [String]
- | ResponseSolveAll [(Int, String)]
- | ResponseJumpToError FilePath Int
- | ResponseEnd
- data DisplayInfo
- = DisplayInfoGeneric String [Block]
- | DisplayInfoAllGoalsWarnings String [Block] [Block] [String] [String]
- | DisplayInfoCurrentGoal Block
- | DisplayInfoInferredType Block
- | DisplayInfoCompilationOk [String] [String]
- | DisplayInfoAuto String
- | DisplayInfoError String
- | DisplayInfoTime String
- | DisplayInfoNormalForm String
- data GiveResult
- data HighlightingInfo = HighlightingInfo Int Int [String] Bool String (Maybe (FilePath, Int))
- data HighlightingInfos = HighlightingInfos Bool [HighlightingInfo]
Documentation
class FromAgda a b | a -> b where Source #
Typeclass for converting Agda values into IR
Instances
FromAgda GiveResult GiveResult Source # | |
Defined in Agda.IR fromAgda :: GiveResult0 -> GiveResult Source # |
class FromAgdaTCM a b | a -> b where Source #
fromAgdaTCM :: a -> TCM b Source #
IR for IOCTM
Instances
data DisplayInfo Source #
IR for DisplayInfo
Instances
data GiveResult Source #
GiveResult
Instances
ToJSON GiveResult Source # | |
Defined in Agda.IR toJSON :: GiveResult -> Value # toEncoding :: GiveResult -> Encoding # toJSONList :: [GiveResult] -> Value # toEncodingList :: [GiveResult] -> Encoding # | |
Generic GiveResult Source # | |
Defined in Agda.IR type Rep GiveResult :: Type -> Type # from :: GiveResult -> Rep GiveResult x # to :: Rep GiveResult x -> GiveResult # | |
FromAgda GiveResult GiveResult Source # | |
Defined in Agda.IR fromAgda :: GiveResult0 -> GiveResult Source # | |
type Rep GiveResult Source # | |
Defined in Agda.IR type Rep GiveResult = D1 ('MetaData "GiveResult" "Agda.IR" "agda-language-server-0.2.6.2.2-9Wn4gKfYowo7ISMsjxvlzN" 'False) (C1 ('MetaCons "GiveString" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: (C1 ('MetaCons "GiveParen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GiveNoParen" 'PrefixI 'False) (U1 :: Type -> Type))) |
data HighlightingInfo Source #
IR for HighlightingInfo
Instances
data HighlightingInfos Source #