Idris2Doc : Idris.Syntax

Idris.Syntax

(source)
Reexports
import public Core.Context
import public Core.Context.Log
import public Core.Normalise
import public Core.Options
import public Idris.Syntax.Pragmas
Definitions
data OpStr' : Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
OpSymbols : nm -> OpStr' nm
  
Backticked : nm -> OpStr' nm

  Hints:
  
Foldable OpStr'
  
Functor OpStr'
  
Show nm => Show (OpStr' nm)
opNameToEither : OpStr' nm -> Either nm nm
  Visibility: export
traverseOp : Functor f => (a -> f b) -> OpStr' a -> f (OpStr' b)
  Visibility: export
.toName : OpStr' nm -> nm
  Visibility: public export
OpStr : Type
  Visibility: public export
data HidingDirective : Type
  Totality: total
  Visibility: public export
  Constructors:
  
HideName : Name -> HidingDirective
  
HideFixity : Fixity -> Name -> HidingDirective
PTerm : Type
  Source language as produced by the parser

  Visibility: public export
IPTerm : Type
  Internal PTerm
  Source language as produced by the unelaboration of core Terms
  KindedNames carry extra information about the nature of the variable

  Visibility: public export
data PTerm' : Type -> Type
  The full high level source language
  This gets desugared to RawImp (TTImp.TTImp),
  then elaborated to Term (Core.TT)

  Totality: total
  Visibility: public export
  Constructors:
  
PRef : FC -> nm -> PTerm' nm
  
NewPi : WithFC (PBinderScope' nm) -> PTerm' nm
  
Forall : WithFC (List1 (WithFC Name), PTerm' nm) -> PTerm' nm
  
PPi : FC -> RigCount -> PiInfo (PTerm' nm) -> Maybe Name -> PTerm' nm -> PTerm' nm -> PTerm' nm
  
PLam : FC -> RigCount -> PiInfo (PTerm' nm) -> PTerm' nm -> PTerm' nm -> PTerm' nm -> PTerm' nm
  
PLet : FC -> RigCount -> PTerm' nm -> PTerm' nm -> PTerm' nm -> PTerm' nm -> List (PClause' nm) -> PTerm' nm
  
PCase : FC -> List (PFnOpt' nm) -> PTerm' nm -> List (PClause' nm) -> PTerm' nm
  
PLocal : FC -> List (PDecl' nm) -> PTerm' nm -> PTerm' nm
  
PUpdate : FC -> List (PFieldUpdate' nm) -> PTerm' nm
  
PApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
  
PWithApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
  
PNamedApp : FC -> PTerm' nm -> Name -> PTerm' nm -> PTerm' nm
  
PAutoApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
  
PDelayed : FC -> LazyReason -> PTerm' nm -> PTerm' nm
  
PDelay : FC -> PTerm' nm -> PTerm' nm
  
PForce : FC -> PTerm' nm -> PTerm' nm
  
PSearch : FC -> Nat -> PTerm' nm
  
PPrimVal : FC -> Constant -> PTerm' nm
  
PQuote : FC -> PTerm' nm -> PTerm' nm
  
PQuoteName : FC -> Name -> PTerm' nm
  
PQuoteDecl : FC -> List (PDecl' nm) -> PTerm' nm
  
PUnquote : FC -> PTerm' nm -> PTerm' nm
  
PRunElab : FC -> PTerm' nm -> PTerm' nm
  
PHole : FC -> Bool -> String -> PTerm' nm
  
PType : FC -> PTerm' nm
  
PAs : FC -> FC -> Name -> PTerm' nm -> PTerm' nm
  
PDotted : FC -> PTerm' nm -> PTerm' nm
  
PImplicit : FC -> PTerm' nm
  
PInfer : FC -> PTerm' nm
  
POp : FC -> WithFC (OperatorLHSInfo (PTerm' nm)) -> WithFC (OpStr' nm) -> PTerm' nm -> PTerm' nm
  
PPrefixOp : FC -> WithFC (OpStr' nm) -> PTerm' nm -> PTerm' nm
  
PSectionL : FC -> WithFC (OpStr' nm) -> PTerm' nm -> PTerm' nm
  
PSectionR : FC -> PTerm' nm -> WithFC (OpStr' nm) -> PTerm' nm
  
PEq : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
  
PBracketed : FC -> PTerm' nm -> PTerm' nm
  
PString : FC -> Nat -> List (PStr' nm) -> PTerm' nm
  
PMultiline : FC -> Nat -> Nat -> List (List (PStr' nm)) -> PTerm' nm
  
PDoBlock : FC -> Maybe Namespace -> List (PDo' nm) -> PTerm' nm
  
PBang : FC -> PTerm' nm -> PTerm' nm
  
PIdiom : FC -> Maybe Namespace -> PTerm' nm -> PTerm' nm
  
PList : FC -> FC -> List (FC, PTerm' nm) -> PTerm' nm
  
PSnocList : FC -> FC -> SnocList (FC, PTerm' nm) -> PTerm' nm
  
PPair : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
  
PDPair : FC -> FC -> PTerm' nm -> PTerm' nm -> PTerm' nm -> PTerm' nm
  
PUnit : FC -> PTerm' nm
  
PIfThenElse : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm -> PTerm' nm
  
PComprehension : FC -> PTerm' nm -> List (PDo' nm) -> PTerm' nm
  
PRewrite : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
  
PRange : FC -> PTerm' nm -> Maybe (PTerm' nm) -> PTerm' nm -> PTerm' nm
  
PRangeStream : FC -> PTerm' nm -> Maybe (PTerm' nm) -> PTerm' nm
  
PPostfixApp : FC -> PTerm' nm -> List (FC, Name) -> PTerm' nm
  
PPostfixAppPartial : FC -> List (FC, Name) -> PTerm' nm
  
PUnifyLog : FC -> LogLevel -> PTerm' nm -> PTerm' nm
  
PWithUnambigNames : FC -> List (FC, Name) -> PTerm' nm -> PTerm' nm
getPTermLoc : PTerm' nm -> FC
  Visibility: export
PFieldUpdate : Type
  Visibility: public export
data PFieldUpdate' : Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
PSetField : List String -> PTerm' nm -> PFieldUpdate' nm
  
PSetFieldApp : List String -> PTerm' nm -> PFieldUpdate' nm
PDo : Type
  Visibility: public export
data PDo' : Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
DoExp : FC -> PTerm' nm -> PDo' nm
  
DoBind : FC -> FC -> Name -> RigCount -> Maybe (PTerm' nm) -> PTerm' nm -> PDo' nm
  
DoBindPat : FC -> PTerm' nm -> Maybe (PTerm' nm) -> PTerm' nm -> List (PClause' nm) -> PDo' nm
  
DoLet : FC -> FC -> Name -> RigCount -> PTerm' nm -> PTerm' nm -> PDo' nm
  
DoLetPat : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm -> List (PClause' nm) -> PDo' nm
  
DoLetLocal : FC -> List (PDecl' nm) -> PDo' nm
  
DoRewrite : FC -> PTerm' nm -> PDo' nm
PStr : Type
  Visibility: public export
data PStr' : Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
StrLiteral : FC -> String -> PStr' nm
  
StrInterp : FC -> PTerm' nm -> PStr' nm
PlainMultiBinder : Type
  Visibility: public export
PlainMultiBinder' : Type -> Type
  A plain binder without information about its use
  plainBinder := name ':' term

  Visibility: public export
PlainBinder : Type
  Visibility: public export
PlainBinder' : Type -> Type
  A plain binder without information about its use
  plainBinder := name ':' term

  Visibility: public export
BasicMultiBinder : Type
  Visibility: public export
record BasicMultiBinder' : Type -> Type
  A binder with quantity information attached
  basicBinder := qty plainBinder

  Totality: total
  Visibility: public export
  Constructor: 
MkBasicMultiBinder : RigCount -> List1 (WithFC Name) -> PTerm' nm -> BasicMultiBinder' nm

  Projections:
  
.names : BasicMultiBinder' nm -> List1 (WithFC Name)
  
.rig : BasicMultiBinder' nm -> RigCount
  
.type : BasicMultiBinder' nm -> PTerm' nm

  Hint: 
Pretty IdrisSyntax (BasicMultiBinder' KindedName)
.rig : BasicMultiBinder' nm -> RigCount
  Visibility: public export
rig : BasicMultiBinder' nm -> RigCount
  Visibility: public export
.names : BasicMultiBinder' nm -> List1 (WithFC Name)
  Visibility: public export
names : BasicMultiBinder' nm -> List1 (WithFC Name)
  Visibility: public export
.type : BasicMultiBinder' nm -> PTerm' nm
  Visibility: public export
type : BasicMultiBinder' nm -> PTerm' nm
  Visibility: public export
PBinder : Type
  Visibility: public export
record PBinder' : Type -> Type
  A binder with information about how it is binding
  pbinder := '{' basicBinder '}'
           | '{' auto basicBinder '}'
           | '{' default term basicBinder '}'
           | '(' basicBinder ')'

  Totality: total
  Visibility: public export
  Constructor: 
MkPBinder : PiInfo (PTerm' nm) -> BasicMultiBinder' nm -> PBinder' nm

  Projections:
  
.bind : PBinder' nm -> BasicMultiBinder' nm
  
.info : PBinder' nm -> PiInfo (PTerm' nm)

  Hint: 
Pretty IdrisSyntax (PBinder' KindedName)
.info : PBinder' nm -> PiInfo (PTerm' nm)
  Visibility: public export
info : PBinder' nm -> PiInfo (PTerm' nm)
  Visibility: public export
.bind : PBinder' nm -> BasicMultiBinder' nm
  Visibility: public export
bind : PBinder' nm -> BasicMultiBinder' nm
  Visibility: public export
PBinderScope : Type
  Visibility: public export
record PBinderScope' : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkPBinderScope : PBinder' nm -> PTerm' nm -> PBinderScope' nm

  Projections:
  
.binder : PBinderScope' nm -> PBinder' nm
  
.scope : PBinderScope' nm -> PTerm' nm
.binder : PBinderScope' nm -> PBinder' nm
  Visibility: public export
binder : PBinderScope' nm -> PBinder' nm
  Visibility: public export
.scope : PBinderScope' nm -> PTerm' nm
  Visibility: public export
scope : PBinderScope' nm -> PTerm' nm
  Visibility: public export
MkFullBinder : PiInfo (PTerm' nm) -> RigCount -> WithFC Name -> PTerm' nm -> PBinder' nm
  Visibility: public export
getLoc : PDo' nm -> FC
  Visibility: export
papply : FC -> PTerm' nm -> List (PTerm' nm) -> PTerm' nm
  Visibility: export
applyArgs : PTerm' nm -> List (FC, PTerm' nm) -> PTerm' nm
  Visibility: export
applyWithArgs : PTerm' nm -> List (FC, PTerm' nm) -> PTerm' nm
  Visibility: export
PTypeDecl : Type
  Visibility: public export
record PTypeDeclData' : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkPTy : List1 (String, WithFC Name) -> String -> PTerm' nm -> PTypeDeclData' nm

  Projections:
  
.doc : PTypeDeclData' nm -> String
  
.names : PTypeDeclData' nm -> List1 (String, WithFC Name)
  
.type : PTypeDeclData' nm -> PTerm' nm
.names : PTypeDeclData' nm -> List1 (String, WithFC Name)
  Visibility: public export
names : PTypeDeclData' nm -> List1 (String, WithFC Name)
  Visibility: public export
.doc : PTypeDeclData' nm -> String
  Visibility: public export
doc : PTypeDeclData' nm -> String
  Visibility: public export
.type : PTypeDeclData' nm -> PTerm' nm
  Visibility: public export
type : PTypeDeclData' nm -> PTerm' nm
  Visibility: public export
PTypeDecl' : Type -> Type
  Visibility: public export
.nameList : PTypeDecl' nm -> List Name
  Visibility: export
PDataDecl : Type
  Visibility: public export
data PDataDecl' : Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
MkPData : FC -> Name -> Maybe (PTerm' nm) -> List DataOpt -> List (PTypeDecl' nm) -> PDataDecl' nm
  
MkPLater : FC -> Name -> PTerm' nm -> PDataDecl' nm
data PRecordDecl' : Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
MkPRecord : Name -> List (PBinder' nm) -> List DataOpt -> Maybe (WithDoc (AddFC Name)) -> List (PField' nm) -> PRecordDecl' nm
  
MkPRecordLater : Name -> List (PBinder' nm) -> PRecordDecl' nm
getPDataDeclLoc : PDataDecl' nm -> FC
  Visibility: export
PWithProblem : Type
  Visibility: public export
record PWithProblem' : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkPWithProblem : RigCount -> PTerm' nm -> Maybe (RigCount, Name) -> PWithProblem' nm

  Projections:
  
.withRigCount : PWithProblem' nm -> RigCount
  
.withRigProof : PWithProblem' nm -> Maybe (RigCount, Name)
  
.withRigValue : PWithProblem' nm -> PTerm' nm
.withRigCount : PWithProblem' nm -> RigCount
  Visibility: public export
withRigCount : PWithProblem' nm -> RigCount
  Visibility: public export
.withRigValue : PWithProblem' nm -> PTerm' nm
  Visibility: public export
withRigValue : PWithProblem' nm -> PTerm' nm
  Visibility: public export
.withRigProof : PWithProblem' nm -> Maybe (RigCount, Name)
  Visibility: public export
withRigProof : PWithProblem' nm -> Maybe (RigCount, Name)
  Visibility: public export
PClause : Type
  Visibility: public export
data PClause' : Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
MkPatClause : FC -> PTerm' nm -> PTerm' nm -> List (PDecl' nm) -> PClause' nm
  
MkWithClause : FC -> PTerm' nm -> List1 (PWithProblem' nm) -> List WithFlag -> List (PClause' nm) -> PClause' nm
  
MkImpossible : FC -> PTerm' nm -> PClause' nm
getPClauseLoc : PClause -> FC
  Visibility: export
data Directive : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Hide : HidingDirective -> Directive
  
Unhide : Name -> Directive
  
Logging : Maybe LogLevel -> Directive
  
LazyOn : Bool -> Directive
  
UnboundImplicits : Bool -> Directive
  
AmbigDepth : Nat -> Directive
  
TotalityDepth : Nat -> Directive
  
PairNames : Name -> Name -> Name -> Directive
  
RewriteName : Name -> Name -> Directive
  
PrimInteger : Name -> Directive
  
PrimString : Name -> Directive
  
PrimChar : Name -> Directive
  
PrimDouble : Name -> Directive
  
PrimTTImp : Name -> Directive
  
PrimName : Name -> Directive
  
PrimDecls : Name -> Directive
  
CGAction : String -> String -> Directive
  
Names : Name -> List String -> Directive
  
StartExpr : PTerm' nm -> Directive
  
Overloadable : Name -> Directive
  
Extension : LangExt -> Directive
  
DefaultTotality : TotalReq -> Directive
  
PrefixRecordProjections : Bool -> Directive
  
AutoImplicitDepth : Nat -> Directive
  
NFMetavarThreshold : Nat -> Directive
  
SearchTimeout : Integer -> Directive
  
ForeignImpl : Name -> List PTerm -> Directive
RecordField' : Type -> Type
  Visibility: public export
PField : Type
  Visibility: public export
PField' : Type -> Type
  Visibility: public export
0 PRecordDeclLet : Type
  Visibility: public export
data PRecordDeclLet' : Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
RecordClaim : WithFC (PClaimData' nm) -> PRecordDeclLet' nm
  
RecordClause : WithFC (PClause' nm) -> PRecordDeclLet' nm
data Pass : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Single : Pass
  
AsType : Pass
  
AsDef : Pass

  Hint: 
Eq Pass
typePass : Pass -> Bool
  Visibility: export
defPass : Pass -> Bool
  Visibility: export
PFnOpt : Type
  Visibility: public export
data PFnOpt' : Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
IFnOpt : FnOpt' nm -> PFnOpt' nm
  
PForeign : List (PTerm' nm) -> PFnOpt' nm
  
PForeignExport : List (PTerm' nm) -> PFnOpt' nm
PClaimData : Type
  Visibility: public export
record PClaimData' : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkPClaim : RigCount -> Visibility -> List (PFnOpt' nm) -> PTypeDecl' nm -> PClaimData' nm

  Projections:
  
.opts : PClaimData' nm -> List (PFnOpt' nm)
  
.qty : PClaimData' nm -> RigCount
  
.type : PClaimData' nm -> PTypeDecl' nm
  
.vis : PClaimData' nm -> Visibility
.qty : PClaimData' nm -> RigCount
  Visibility: public export
qty : PClaimData' nm -> RigCount
  Visibility: public export
.vis : PClaimData' nm -> Visibility
  Visibility: public export
vis : PClaimData' nm -> Visibility
  Visibility: public export
.opts : PClaimData' nm -> List (PFnOpt' nm)
  Visibility: public export
opts : PClaimData' nm -> List (PFnOpt' nm)
  Visibility: public export
.type : PClaimData' nm -> PTypeDecl' nm
  Visibility: public export
type : PClaimData' nm -> PTypeDecl' nm
  Visibility: public export
record PFixityData : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkPFixityData : WithDefault Visibility Export -> BindingModifier -> Fixity -> Nat -> List1 OpStr -> PFixityData

  Projections:
  
.binding : PFixityData -> BindingModifier
  
.exportModifier : PFixityData -> WithDefault Visibility Export
  
.fixity : PFixityData -> Fixity
  
.operators : PFixityData -> List1 OpStr
  
.precedence : PFixityData -> Nat
.exportModifier : PFixityData -> WithDefault Visibility Export
  Visibility: public export
exportModifier : PFixityData -> WithDefault Visibility Export
  Visibility: public export
.binding : PFixityData -> BindingModifier
  Visibility: public export
binding : PFixityData -> BindingModifier
  Visibility: public export
.fixity : PFixityData -> Fixity
  Visibility: public export
fixity : PFixityData -> Fixity
  Visibility: public export
.precedence : PFixityData -> Nat
  Visibility: public export
precedence : PFixityData -> Nat
  Visibility: public export
.operators : PFixityData -> List1 OpStr
  Visibility: public export
operators : PFixityData -> List1 OpStr
  Visibility: public export
PDecl : Type
  Visibility: public export
data PDeclNoFC' : Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
PClaim : PClaimData' nm -> PDeclNoFC' nm
  
PDef : List (PClause' nm) -> PDeclNoFC' nm
  
PData : String -> WithDefault Visibility Private -> Maybe TotalReq -> PDataDecl' nm -> PDeclNoFC' nm
  
PParameters : Either (List1 (PlainBinder' nm)) (List1 (PBinder' nm)) -> List (PDecl' nm) -> PDeclNoFC' nm
  
PUsing : List (Maybe Name, PTerm' nm) -> List (PDecl' nm) -> PDeclNoFC' nm
  
PInterface : WithDefault Visibility Private -> List (Maybe Name, PTerm' nm) -> Name -> String -> List (BasicMultiBinder' nm) -> Maybe (List1 Name) -> Maybe (WithDoc (AddFC Name)) -> List (PDecl' nm) -> PDeclNoFC' nm
  
PImplementation : Visibility -> List PFnOpt -> Pass -> List (AddFC (ImpParameter' (PTerm' nm))) -> List (Maybe Name, PTerm' nm) -> Name -> List (PTerm' nm) -> Maybe Name -> List Name -> Maybe (List (PDecl' nm)) -> PDeclNoFC' nm
  
PRecord : String -> WithDefault Visibility Private -> Maybe TotalReq -> PRecordDecl' nm -> PDeclNoFC' nm
  
PFail : Maybe String -> List (PDecl' nm) -> PDeclNoFC' nm
  PFail is a failing block. The string must appear as a
  substring of the error message raised when checking the block.
  
PMutual : List (PDecl' nm) -> PDeclNoFC' nm
  
PFixity : PFixityData -> PDeclNoFC' nm
  
PNamespace : Namespace -> List (PDecl' nm) -> PDeclNoFC' nm
  
PTransform : String -> PTerm' nm -> PTerm' nm -> PDeclNoFC' nm
  
PRunElabDecl : PTerm' nm -> PDeclNoFC' nm
  
PDirective : Directive -> PDeclNoFC' nm
  
PBuiltin : BuiltinType -> Name -> PDeclNoFC' nm
PDeclNoFC : Type
  Visibility: public export
PDecl' : Type -> Type
  Visibility: public export
getPDeclLoc : PDecl' nm -> FC
  Visibility: export
isStrInterp : PStr -> Maybe FC
  Visibility: export
isStrLiteral : PStr -> Maybe (FC, String)
  Visibility: export
isPDef : PDecl -> Maybe (WithFC (List PClause))
  Visibility: export
definedIn : List PDeclNoFC -> List Name
  Visibility: export
data REPLEval : Type
  Totality: total
  Visibility: public export
  Constructors:
  
EvalTC : REPLEval
  
NormaliseAll : REPLEval
  
Execute : REPLEval
  
Scheme : REPLEval

  Hints:
  
Cast REPLEval String
  
Pretty Void REPLEval
  
Show REPLEval
data REPLOpt : Type
  Totality: total
  Visibility: public export
  Constructors:
  
ShowImplicits : Bool -> REPLOpt
  
ShowNamespace : Bool -> REPLOpt
  
ShowMachineNames : Bool -> REPLOpt
  
ShowTypes : Bool -> REPLOpt
  
EvalMode : REPLEval -> REPLOpt
  
Editor : String -> REPLOpt
  
CG : String -> REPLOpt
  
Profile : Bool -> REPLOpt
  
EvalTiming : Bool -> REPLOpt

  Hints:
  
Cast REPLOpt REPLOption
  
Pretty Void REPLOpt
  
Show REPLOpt
data EditCmd : Type
  Totality: total
  Visibility: public export
  Constructors:
  
TypeAt : Int -> Int -> Name -> EditCmd
  
CaseSplit : Bool -> Int -> Int -> Name -> EditCmd
  
AddClause : Bool -> Int -> Name -> EditCmd
  
Refine : Bool -> Int -> Name -> PTerm -> EditCmd
  
Intro : Bool -> Int -> Name -> EditCmd
  
ExprSearch : Bool -> Int -> Name -> List Name -> EditCmd
  
ExprSearchNext : EditCmd
  
GenerateDef : Bool -> Int -> Name -> Nat -> EditCmd
  
GenerateDefNext : EditCmd
  
MakeLemma : Bool -> Int -> Name -> EditCmd
  
MakeCase : Bool -> Int -> Name -> EditCmd
  
MakeWith : Bool -> Int -> Name -> EditCmd
data BracketType : Type
  Totality: total
  Visibility: public export
  Constructors:
  
IdiomBrackets : BracketType
  
NameQuote : BracketType
  
TermQuote : BracketType
  
DeclQuote : BracketType
data DocDirective : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Keyword : String -> DocDirective
  A reserved keyword
  
Symbol : String -> DocDirective
  A reserved symbol
  
Bracket : BracketType -> DocDirective
  A type of brackets
  
APTerm : PTerm -> DocDirective
  An arbitrary PTerm
  
AModule : ModuleIdent -> DocDirective
  A module name
data HelpType : Type
  Totality: total
  Visibility: public export
  Constructors:
  
GenericHelp : HelpType
  
DetailedHelp : String -> HelpType
data REPLCmd : Type
  Totality: total
  Visibility: public export
  Constructors:
  
NewDefn : List PDecl -> REPLCmd
  
Eval : PTerm -> REPLCmd
  
Check : PTerm -> REPLCmd
  
CheckWithImplicits : PTerm -> REPLCmd
  
PrintDef : PTerm -> REPLCmd
  
Reload : REPLCmd
  
Load : String -> REPLCmd
  
ImportMod : ModuleIdent -> REPLCmd
  
Edit : REPLCmd
  
Compile : PTerm -> String -> REPLCmd
  
Exec : PTerm -> REPLCmd
  
Help : HelpType -> REPLCmd
  
TypeSearch : PTerm -> REPLCmd
  
FuzzyTypeSearch : PTerm -> REPLCmd
  
DebugInfo : Name -> REPLCmd
  
SetOpt : REPLOpt -> REPLCmd
  
GetOpts : REPLCmd
  
CGDirective : String -> REPLCmd
  
CD : String -> REPLCmd
  
CWD : REPLCmd
  
Missing : Name -> REPLCmd
  
Total : Name -> REPLCmd
  
Doc : DocDirective -> REPLCmd
  
Browse : Namespace -> REPLCmd
  
SetLog : Maybe LogLevel -> REPLCmd
  
SetConsoleWidth : Maybe Nat -> REPLCmd
  
SetColor : Bool -> REPLCmd
  
Metavars : REPLCmd
  
Editing : EditCmd -> REPLCmd
  
RunShellCommand : String -> REPLCmd
  
ShowVersion : REPLCmd
  
Quit : REPLCmd
  
NOP : REPLCmd
  
ImportPackage : String -> REPLCmd
record Import : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkImport : FC -> Bool -> ModuleIdent -> Namespace -> Import

  Projections:
  
.loc : Import -> FC
  
.nameAs : Import -> Namespace
  
.path : Import -> ModuleIdent
  
.reexport : Import -> Bool

  Hints:
  
Show Import
  
TTC Import
.loc : Import -> FC
  Visibility: public export
loc : Import -> FC
  Visibility: public export
.reexport : Import -> Bool
  Visibility: public export
reexport : Import -> Bool
  Visibility: public export
.path : Import -> ModuleIdent
  Visibility: public export
path : Import -> ModuleIdent
  Visibility: public export
.nameAs : Import -> Namespace
  Visibility: public export
nameAs : Import -> Namespace
  Visibility: public export
record Module : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkModule : FC -> ModuleIdent -> List Import -> String -> List PDecl -> Module

  Projections:
  
.decls : Module -> List PDecl
  
.documentation : Module -> String
  
.headerLoc : Module -> FC
  
.imports : Module -> List Import
  
.moduleNS : Module -> ModuleIdent
.headerLoc : Module -> FC
  Visibility: public export
headerLoc : Module -> FC
  Visibility: public export
.moduleNS : Module -> ModuleIdent
  Visibility: public export
moduleNS : Module -> ModuleIdent
  Visibility: public export
.imports : Module -> List Import
  Visibility: public export
imports : Module -> List Import
  Visibility: public export
.documentation : Module -> String
  Visibility: public export
documentation : Module -> String
  Visibility: public export
.decls : Module -> List PDecl
  Visibility: public export
decls : Module -> List PDecl
  Visibility: public export
0 Method : Type
  Visibility: public export
record IFaceInfo : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkIFaceInfo : Name -> List Name -> List Name -> List RawImp -> List Method -> List (Name, List ImpClause) -> IFaceInfo

  Projections:
  
.defaults : IFaceInfo -> List (Name, List ImpClause)
  
.iconstructor : IFaceInfo -> Name
  
.implParams : IFaceInfo -> List Name
  
.methods : IFaceInfo -> List Method
  
.params : IFaceInfo -> List Name
  
.parents : IFaceInfo -> List RawImp

  Hints:
  
HasNames IFaceInfo
  
TTC IFaceInfo
.iconstructor : IFaceInfo -> Name
  Visibility: public export
iconstructor : IFaceInfo -> Name
  Visibility: public export
.implParams : IFaceInfo -> List Name
  Visibility: public export
implParams : IFaceInfo -> List Name
  Visibility: public export
.params : IFaceInfo -> List Name
  Visibility: public export
params : IFaceInfo -> List Name
  Visibility: public export
.parents : IFaceInfo -> List RawImp
  Visibility: public export
parents : IFaceInfo -> List RawImp
  Visibility: public export
.methods : IFaceInfo -> List Method
  Visibility: public export
methods : IFaceInfo -> List Method
  Visibility: public export
.defaults : IFaceInfo -> List (Name, List ImpClause)
  Visibility: public export
defaults : IFaceInfo -> List (Name, List ImpClause)
  Visibility: public export
record SyntaxInfo : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkSyntax : ANameMap FixityInfo -> List ModuleIdent -> SortedMap ModuleIdent String -> SortedMap ModuleIdent (List Import) -> List Name -> ANameMap IFaceInfo -> NameMap () -> ANameMap String -> List Name -> List (Maybe Name, RawImp) -> RawImp -> List String -> SyntaxInfo

  Projections:
  
.bracketholes : SyntaxInfo -> List Name
  
.defDocstrings : SyntaxInfo -> ANameMap String
  
.fixities : SyntaxInfo -> ANameMap FixityInfo
  Operators fixities as a map from their names to their fixity,
  precedence, and the file context where that fixity was defined.
  
.holeNames : SyntaxInfo -> List String
  
.ifaces : SyntaxInfo -> ANameMap IFaceInfo
  
.modDocexports : SyntaxInfo -> SortedMap ModuleIdent (List Import)
  
.modDocstrings : SyntaxInfo -> SortedMap ModuleIdent String
  
.saveDocstrings : SyntaxInfo -> NameMap ()
  
.saveIFaces : SyntaxInfo -> List Name
  
.saveMod : SyntaxInfo -> List ModuleIdent
  
.startExpr : SyntaxInfo -> RawImp
  
.usingImpl : SyntaxInfo -> List (Maybe Name, RawImp)

  Hints:
  
HasNames SyntaxInfo
  
TTC SyntaxInfo
.fixities : SyntaxInfo -> ANameMap FixityInfo
  Operators fixities as a map from their names to their fixity,
  precedence, and the file context where that fixity was defined.

  Visibility: public export
fixities : SyntaxInfo -> ANameMap FixityInfo
  Operators fixities as a map from their names to their fixity,
  precedence, and the file context where that fixity was defined.

  Visibility: public export
.saveMod : SyntaxInfo -> List ModuleIdent
  Visibility: public export
saveMod : SyntaxInfo -> List ModuleIdent
  Visibility: public export
.modDocstrings : SyntaxInfo -> SortedMap ModuleIdent String
  Visibility: public export
modDocstrings : SyntaxInfo -> SortedMap ModuleIdent String
  Visibility: public export
.modDocexports : SyntaxInfo -> SortedMap ModuleIdent (List Import)
  Visibility: public export
modDocexports : SyntaxInfo -> SortedMap ModuleIdent (List Import)
  Visibility: public export
.saveIFaces : SyntaxInfo -> List Name
  Visibility: public export
saveIFaces : SyntaxInfo -> List Name
  Visibility: public export
.ifaces : SyntaxInfo -> ANameMap IFaceInfo
  Visibility: public export
ifaces : SyntaxInfo -> ANameMap IFaceInfo
  Visibility: public export
.saveDocstrings : SyntaxInfo -> NameMap ()
  Visibility: public export
saveDocstrings : SyntaxInfo -> NameMap ()
  Visibility: public export
.defDocstrings : SyntaxInfo -> ANameMap String
  Visibility: public export
defDocstrings : SyntaxInfo -> ANameMap String
  Visibility: public export
.bracketholes : SyntaxInfo -> List Name
  Visibility: public export
bracketholes : SyntaxInfo -> List Name
  Visibility: public export
.usingImpl : SyntaxInfo -> List (Maybe Name, RawImp)
  Visibility: public export
usingImpl : SyntaxInfo -> List (Maybe Name, RawImp)
  Visibility: public export
.startExpr : SyntaxInfo -> RawImp
  Visibility: public export
startExpr : SyntaxInfo -> RawImp
  Visibility: public export
.holeNames : SyntaxInfo -> List String
  Visibility: public export
holeNames : SyntaxInfo -> List String
  Visibility: public export
prefixes : SyntaxInfo -> ANameMap (FC, Nat)
  Visibility: export
infixes : SyntaxInfo -> ANameMap (FC, (Fixity, Nat))
  Visibility: export
initSyntax : SyntaxInfo
  Visibility: export
data Syn : Type
  Totality: total
  Visibility: export
withSyn : Ref Syn SyntaxInfo => Core a -> Core a
  Visibility: export
addModDocInfo : Ref Syn SyntaxInfo => ModuleIdent -> String -> List Import -> Core ()
  Visibility: export
removeFixity : Ref Syn SyntaxInfo => FC -> Fixity -> Name -> Core ()
  Remove a fixity from the context

  Visibility: export
getFixityInfo : Ref Syn SyntaxInfo => String -> Core (List (Name, FixityInfo))
  Return all fixity declarations for an operator name

  Visibility: export