Idris2Doc : Core.Core

Core.Core

(source)
Reexports
import public Core.WithData
import public Data.IORef
Definitions
data TTCErrorMsg : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Format : String -> Int -> Int -> TTCErrorMsg
  
EndOfBuffer : String -> TTCErrorMsg
  
Corrupt : String -> TTCErrorMsg

  Hint: 
Show TTCErrorMsg
data CaseError : Type
  Totality: total
  Visibility: public export
  Constructors:
  
DifferingArgNumbers : CaseError
  
DifferingTypes : CaseError
  
MatchErased : (vars : List Name ** (Env Term vars, Term vars)) -> CaseError
  
NotFullyApplied : Name -> CaseError
  
UnknownType : CaseError

  Hint: 
HasNames CaseError
data DotReason : Type
  Totality: total
  Visibility: public export
  Constructors:
  
NonLinearVar : DotReason
  
VarApplied : DotReason
  
NotConstructor : DotReason
  
ErasedArg : DotReason
  
UserDotted : DotReason
  
UnknownDot : DotReason
  
UnderAppliedCon : DotReason

  Hints:
  
Pretty ann DotReason
  
Show DotReason
data Warning : Type
  Totality: total
  Visibility: public export
  Constructors:
  
ParserWarning : FC -> String -> Warning
  
UnreachableClause : FC -> Env Term vars -> Term vars -> Warning
  
ShadowingGlobalDefs : FC -> List1 (Name, List1 Name) -> Warning
  
IncompatibleVisibility : FC -> Visibility -> Visibility -> Name -> Warning
  Soft-breaking change, make an error later.
  @ original Originally declared visibility on forward decl
  @ new      Incompatible new visibility on actual declaration.
  
ShadowingLocalBindings : FC -> List1 (String, (FC, FC)) -> Warning
  First FC is type
  @ shadowed list of names which are shadowed,
    where they originally appear
    and where they are shadowed
  
Deprecated : FC -> String -> Maybe (FC, Name) -> Warning
  A warning about a deprecated definition. Supply an FC and Name to
  have the documentation for the definition printed with the warning.
  
GenericWarn : FC -> String -> Warning

  Hints:
  
HasNames Warning
  
Show Warning
data Error : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Fatal : Error -> Error
  
CantConvert : FC -> Context -> Env Term vars -> Term vars -> Term vars -> Error
  
CantSolveEq : FC -> Context -> Env Term vars -> Term vars -> Term vars -> Error
  
PatternVariableUnifies : FC -> FC -> Env Term vars -> Name -> Term vars -> Error
  
CyclicMeta : FC -> Env Term vars -> Name -> Term vars -> Error
  
WhenUnifying : FC -> Context -> Env Term vars -> Term vars -> Term vars -> Error -> Error
  
ValidCase : FC -> Env Term vars -> Either (Term vars) Error -> Error
  
UndefinedName : FC -> Name -> Error
  
InvisibleName : FC -> Name -> Maybe Namespace -> Error
  
BadTypeConType : FC -> Name -> Error
  
BadDataConType : FC -> Name -> Name -> Error
  
NotCovering : FC -> Name -> Covering -> Error
  
NotTotal : FC -> Name -> PartialReason -> Error
  
ImpossibleCase : Error
  
LinearUsed : FC -> Nat -> Name -> Error
  
LinearMisuse : FC -> Name -> RigCount -> RigCount -> Error
  
BorrowPartial : FC -> Env Term vars -> Term vars -> Term vars -> Error
  
BorrowPartialType : FC -> Env Term vars -> Term vars -> Error
  
AmbiguousName : FC -> List Name -> Error
  
AmbiguousElab : FC -> Env Term vars -> List (Context, Term vars) -> Error
  
AmbiguousSearch : FC -> Env Term vars -> Term vars -> List (Term vars) -> Error
  
AmbiguityTooDeep : FC -> Name -> List Name -> Error
  
AllFailed : List (Maybe Name, Error) -> Error
  
RecordTypeNeeded : FC -> Env Term vars -> Error
  
DuplicatedRecordUpdatePath : FC -> List (List String) -> Error
  
NotRecordField : FC -> String -> Maybe Name -> Error
  
NotRecordType : FC -> Name -> Error
  
IncompatibleFieldUpdate : FC -> List String -> Error
  
InvalidArgs : FC -> Env Term vars -> List Name -> Term vars -> Error
  
TryWithImplicits : FC -> Env Term vars -> List (Name, Term vars) -> Error
  
BadUnboundImplicit : FC -> Env Term vars -> Name -> Term vars -> Error
  
CantSolveGoal : FC -> Context -> Env Term vars -> Term vars -> Maybe Error -> Error
  
DeterminingArg : FC -> Name -> Int -> Env Term vars -> Term vars -> Error
  
UnsolvedHoles : List (FC, Name) -> Error
  
CantInferArgType : FC -> Env Term vars -> Name -> Name -> Term vars -> Error
  
SolvedNamedHole : FC -> Env Term vars -> Name -> Term vars -> Error
  
VisibilityError : FC -> Visibility -> Name -> Visibility -> Name -> Error
  
NonLinearPattern : FC -> Name -> Error
  
BadPattern : FC -> Name -> Error
  
NoDeclaration : FC -> Name -> Error
  
AlreadyDefined : FC -> Name -> Error
  
NotFunctionType : FC -> Env Term vars -> Term vars -> Error
  
RewriteNoChange : FC -> Env Term vars -> Term vars -> Term vars -> Error
  
NotRewriteRule : FC -> Env Term vars -> Term vars -> Error
  
CaseCompile : FC -> Name -> CaseError -> Error
  
MatchTooSpecific : FC -> Env Term vars -> Term vars -> Error
  
BadDotPattern : FC -> Env Term vars -> DotReason -> Term vars -> Term vars -> Error
  
BadImplicit : FC -> String -> Error
  
BadRunElab : FC -> Env Term vars -> Term vars -> String -> Error
  
RunElabFail : Error -> Error
  
GenericMsg : FC -> String -> Error
  
GenericMsgSol : FC -> String -> String -> List String -> Error
  
OperatorBindingMismatch : FC -> FixityDeclarationInfo -> OperatorLHSInfo a -> Either Name Name -> a -> List String -> Error
  
TTCError : TTCErrorMsg -> Error
  
FileErr : String -> FileError -> Error
  
CantFindPackage : String -> Error
  
LazyImplicitFunction : FC -> Error
  
LazyPatternVar : FC -> Error
  
LitFail : FC -> Error
  
LexFail : FC -> String -> Error
  
ParseFail : List1 (FC, String) -> Error
  
ModuleNotFound : FC -> ModuleIdent -> Error
  
CyclicImports : List ModuleIdent -> Error
  
ForceNeeded : Error
  
InternalError : String -> Error
  
UserError : String -> Error
  
NoForeignCC : FC -> List String -> Error
  Contains list of specifiers for which foreign call cannot be resolved
  
BadMultiline : FC -> String -> Error
  
Timeout : String -> Error
  
FailingDidNotFail : FC -> Error
  
FailingWrongError : FC -> String -> List1 Error -> Error
  
InType : FC -> Name -> Error -> Error
  
InCon : WithFC Name -> Error -> Error
  
InLHS : FC -> Name -> Error -> Error
  
InRHS : FC -> Name -> Error -> Error
  
MaybeMisspelling : Error -> List1 String -> Error
  
WarningAsError : Warning -> Error

  Hints:
  
Catchable Core Error
  
HasNames Error
  
Show Error
getWarningLoc : Warning -> FC
  Visibility: export
getErrorLoc : Error -> Maybe FC
  Visibility: export
killWarningLoc : Warning -> Warning
  Visibility: export
killErrorLoc : Error -> Error
  Visibility: export
record Core : Type -> Type
  Totality: total
  Visibility: export
  Constructor: 
MkCore : IO (Either Error t) -> Core t

  Projection: 
.runCore : Core t -> IO (Either Error t)

  Hint: 
Catchable Core Error
coreRun : Core a -> (Error -> IO b) -> (a -> IO b) -> IO b
  Visibility: export
coreFail : Error -> Core a
  Visibility: export
wrapError : (Error -> Error) -> Core a -> Core a
  Visibility: export
coreLift : IO a -> Core a
  Visibility: export
map : (a -> b) -> Core a -> Core b
  Visibility: export
(<$>) : (a -> b) -> Core a -> Core b
  Visibility: export
  Fixity Declaration: infixr operator, level 4
(<$) : b -> Core a -> Core b
  Visibility: export
  Fixity Declaration: infixr operator, level 4
ignore : Core a -> Core ()
  Visibility: export
coreLift_ : IO a -> Core ()
  Visibility: export
(>>=) : Core a -> (a -> Core b) -> Core b
  Visibility: export
  Fixity Declaration: infixl operator, level 1
(>>) : Core () -> Core a -> Core a
  Visibility: export
  Fixity Declaration: infixl operator, level 1
(=<<) : (a -> Core b) -> Core a -> Core b
  Visibility: export
  Fixity Declaration: infixl operator, level 1
(>=>) : (a -> Core b) -> (b -> Core c) -> a -> Core c
  Visibility: export
  Fixity Declaration: infixl operator, level 1
(<=<) : (b -> Core c) -> (a -> Core b) -> a -> Core c
  Visibility: export
  Fixity Declaration: infixl operator, level 1
pure : a -> Core a
  Visibility: export
(<*>) : Core (a -> b) -> Core a -> Core b
  Visibility: export
  Fixity Declaration: infixl operator, level 3
(*>) : Core a -> Core b -> Core b
  Visibility: export
  Fixity Declaration: infixl operator, level 3
(<*) : Core a -> Core b -> Core a
  Visibility: export
  Fixity Declaration: infixl operator, level 3
when : Bool -> Lazy (Core ()) -> Core ()
  Visibility: export
unless : Bool -> Lazy (Core ()) -> Core ()
  Visibility: export
iwhen : (b : Bool) -> Lazy (Core a) -> Core (IMaybe b a)
  Visibility: export
iunless : (b : Bool) -> Lazy (Core a) -> Core (IMaybe (not b) a)
  Visibility: export
whenJust : Maybe a -> (a -> Core ()) -> Core ()
  Visibility: export
iwhenJust : IMaybe b a -> (a -> Core ()) -> Core ()
  Visibility: export
interface Catchable : (Type -> Type) -> Type -> Type
  Parameters: m, t
Methods:
  
throw : t -> m a
  
catch : m a -> (t -> m a) -> m a
  
breakpoint : m a -> m (Either t a)

Implementation: 
Catchable Core Error
throw : Catchable m t => t -> m a
  Visibility: public export
catch : Catchable m t => m a -> (t -> m a) -> m a
  Visibility: public export
breakpoint : Catchable m t => m a -> m (Either t a)
  Visibility: public export
foldlC : Foldable t => (a -> b -> Core a) -> a -> t b -> Core a
  Visibility: export
traverse : (a -> Core b) -> List a -> Core (List b)
  Visibility: export
traverse : (a -> Core b) -> SnocList a -> Core (SnocList b)
  Visibility: export
mapMaybeM : (a -> Core (Maybe b)) -> List a -> Core (List b)
  Visibility: export
for : List a -> (a -> Core b) -> Core (List b)
  Visibility: export
traverseList1 : (a -> Core b) -> List1 a -> Core (List1 b)
  Visibility: export
traverseSnocList : (a -> Core b) -> SnocList a -> Core (SnocList b)
  Visibility: export
traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b)
  Visibility: export
traverseList01 : (a -> Core b) -> List01 ne a -> Core (List01 ne b)
  Visibility: export
traverseOpt : (a -> Core b) -> Maybe a -> Core (Maybe b)
  Visibility: export
traversePair : (a -> Core b) -> (w, a) -> Core (w, b)
  Visibility: export
traverse_ : (a -> Core b) -> List a -> Core ()
  Visibility: export
for_ : List a -> (a -> Core ()) -> Core ()
  Visibility: export
sequence : List (Core a) -> Core (List a)
  Visibility: export
traverseList1_ : (a -> Core b) -> List1 a -> Core ()
  Visibility: export
traverse_ : (a -> Core b) -> SnocList a -> Core ()
  Visibility: export
traverse : (ty -> Core sy) -> WithData fs ty -> Core (WithData fs sy)
  Visibility: export
traverse : (a -> Core b) -> PiInfo a -> Core (PiInfo b)
  Visibility: export
traverse : (a -> Core b) -> PiBindData a -> Core (PiBindData b)
  Visibility: export
traverse : (a -> Core b) -> Binder a -> Core (Binder b)
  Visibility: export
mapTermM : (Term vars -> Core (Term vars)) -> Term vars -> Core (Term vars)
  Visibility: export
anyM : (a -> Core Bool) -> List a -> Core Bool
  Visibility: export
anyM : (a -> Core Bool) -> SnocList a -> Core Bool
  Visibility: export
allM : (a -> Core Bool) -> List a -> Core Bool
  Visibility: export
filterM : (a -> Core Bool) -> List a -> Core (List a)
  Visibility: export
newRef : (0 x : label) -> t -> Core (Ref x t)
  Visibility: export
get : (0 x : label) -> Ref x a => Core a
  Visibility: export
put : (0 x : label) -> Ref x a => a -> Core ()
  Visibility: export
update : (0 x : label) -> Ref x a => (a -> a) -> Core ()
  Visibility: export
wrapRef : (0 x : label) -> Ref x a => (a -> Core ()) -> Core b -> Core b
  Visibility: export
cond : List (Lazy Bool, Lazy a) -> Lazy a -> a
  Visibility: export
condC : List (Core Bool, Core a) -> Core a -> Core a
  Visibility: export
writeFile : String -> String -> Core ()
  Visibility: export
readFile : String -> Core String
  Visibility: export
Search : Type -> Type
  Visibility: public export
functor : Functor Search
  Visibility: export
traverse : (a -> Core b) -> Search a -> Core (Search b)
  Visibility: export
filter : (a -> Bool) -> Search a -> Core (Search a)
  Visibility: export