Idris2Doc : Core.Options

Core.Options

(source)
Reexports
import public Core.Options.Log
Definitions
record Dirs : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkDirs : String -> Maybe String -> String -> String -> Maybe String -> String -> List String -> List Path -> List String -> List String -> List String -> Dirs

  Projections:
  
.build_dir : Dirs -> String
  
.data_dirs : Dirs -> List String
  
.depends_dir : Dirs -> String
  
.extra_dirs : Dirs -> List String
  
.lib_dirs : Dirs -> List String
  
.output_dir : Dirs -> Maybe String
  
.package_dirs : Dirs -> List String
  
.package_search_paths : Dirs -> List Path
  
.prefix_dir : Dirs -> String
  
.source_dir : Dirs -> Maybe String
  
.working_dir : Dirs -> String
.working_dir : Dirs -> String
  Totality: total
  Visibility: public export
working_dir : Dirs -> String
  Totality: total
  Visibility: public export
.source_dir : Dirs -> Maybe String
  Totality: total
  Visibility: public export
source_dir : Dirs -> Maybe String
  Totality: total
  Visibility: public export
.build_dir : Dirs -> String
  Totality: total
  Visibility: public export
build_dir : Dirs -> String
  Totality: total
  Visibility: public export
.depends_dir : Dirs -> String
  Totality: total
  Visibility: public export
depends_dir : Dirs -> String
  Totality: total
  Visibility: public export
.output_dir : Dirs -> Maybe String
  Totality: total
  Visibility: public export
output_dir : Dirs -> Maybe String
  Totality: total
  Visibility: public export
.prefix_dir : Dirs -> String
  Totality: total
  Visibility: public export
prefix_dir : Dirs -> String
  Totality: total
  Visibility: public export
.extra_dirs : Dirs -> List String
  Totality: total
  Visibility: public export
extra_dirs : Dirs -> List String
  Totality: total
  Visibility: public export
.package_search_paths : Dirs -> List Path
  Totality: total
  Visibility: public export
package_search_paths : Dirs -> List Path
  Totality: total
  Visibility: public export
.package_dirs : Dirs -> List String
  Totality: total
  Visibility: public export
package_dirs : Dirs -> List String
  Totality: total
  Visibility: public export
.lib_dirs : Dirs -> List String
  Totality: total
  Visibility: public export
lib_dirs : Dirs -> List String
  Totality: total
  Visibility: public export
.data_dirs : Dirs -> List String
  Totality: total
  Visibility: public export
data_dirs : Dirs -> List String
  Totality: total
  Visibility: public export
execBuildDir : Dirs -> String
  Totality: total
  Visibility: export
outputDirWithDefault : Dirs -> String
  Totality: total
  Visibility: export
toString : Dirs -> String
  Totality: total
  Visibility: public export
data CG : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Chez : CG
  
ChezSep : CG
  
Racket : CG
  
Gambit : CG
  
Node : CG
  
Javascript : CG
  
RefC : CG
  
VMCodeInterp : CG
  
Other : String -> CG

  Hints:
  
Eq CG
  
Show CG
  
TTC CG
record PairNames : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkPairNs : Name -> Name -> Name -> PairNames

  Projections:
  
.fstName : PairNames -> Name
  
.pairType : PairNames -> Name
  
.sndName : PairNames -> Name

  Hint: 
TTC PairNames
.pairType : PairNames -> Name
  Totality: total
  Visibility: public export
pairType : PairNames -> Name
  Totality: total
  Visibility: public export
.fstName : PairNames -> Name
  Totality: total
  Visibility: public export
fstName : PairNames -> Name
  Totality: total
  Visibility: public export
.sndName : PairNames -> Name
  Totality: total
  Visibility: public export
sndName : PairNames -> Name
  Totality: total
  Visibility: public export
record RewriteNames : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkRewriteNs : Name -> Name -> RewriteNames

  Projections:
  
.equalType : RewriteNames -> Name
  
.rewriteName : RewriteNames -> Name

  Hint: 
TTC RewriteNames
.equalType : RewriteNames -> Name
  Totality: total
  Visibility: public export
equalType : RewriteNames -> Name
  Totality: total
  Visibility: public export
.rewriteName : RewriteNames -> Name
  Totality: total
  Visibility: public export
rewriteName : RewriteNames -> Name
  Totality: total
  Visibility: public export
record PrimNames : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkPrimNs : Maybe Name -> Maybe Name -> Maybe Name -> Maybe Name -> Maybe Name -> Maybe Name -> Maybe Name -> PrimNames

  Projections:
  
.fromCharName : PrimNames -> Maybe Name
  
.fromDeclsName : PrimNames -> Maybe Name
  
.fromDoubleName : PrimNames -> Maybe Name
  
.fromIntegerName : PrimNames -> Maybe Name
  
.fromNameName : PrimNames -> Maybe Name
  
.fromStringName : PrimNames -> Maybe Name
  
.fromTTImpName : PrimNames -> Maybe Name

  Hint: 
TTC PrimNames
.fromIntegerName : PrimNames -> Maybe Name
  Totality: total
  Visibility: public export
fromIntegerName : PrimNames -> Maybe Name
  Totality: total
  Visibility: public export
.fromStringName : PrimNames -> Maybe Name
  Totality: total
  Visibility: public export
fromStringName : PrimNames -> Maybe Name
  Totality: total
  Visibility: public export
.fromCharName : PrimNames -> Maybe Name
  Totality: total
  Visibility: public export
fromCharName : PrimNames -> Maybe Name
  Totality: total
  Visibility: public export
.fromDoubleName : PrimNames -> Maybe Name
  Totality: total
  Visibility: public export
fromDoubleName : PrimNames -> Maybe Name
  Totality: total
  Visibility: public export
.fromTTImpName : PrimNames -> Maybe Name
  Totality: total
  Visibility: public export
fromTTImpName : PrimNames -> Maybe Name
  Totality: total
  Visibility: public export
.fromNameName : PrimNames -> Maybe Name
  Totality: total
  Visibility: public export
fromNameName : PrimNames -> Maybe Name
  Totality: total
  Visibility: public export
.fromDeclsName : PrimNames -> Maybe Name
  Totality: total
  Visibility: public export
fromDeclsName : PrimNames -> Maybe Name
  Totality: total
  Visibility: public export
primNamesToList : PrimNames -> List Name
  Totality: total
  Visibility: export
record ElabDirectives : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkElabDirectives : Bool -> Bool -> TotalReq -> Nat -> Nat -> Nat -> Nat -> Bool -> ElabDirectives

  Projections:
  
.ambigLimit : ElabDirectives -> Nat
  
.autoImplicitLimit : ElabDirectives -> Nat
  
.lazyActive : ElabDirectives -> Bool
  
.nfThreshold : ElabDirectives -> Nat
  
.prefixRecordProjections : ElabDirectives -> Bool
  
.totalLimit : ElabDirectives -> Nat
  
.totality : ElabDirectives -> TotalReq
  
.unboundImplicits : ElabDirectives -> Bool
.lazyActive : ElabDirectives -> Bool
  Totality: total
  Visibility: public export
lazyActive : ElabDirectives -> Bool
  Totality: total
  Visibility: public export
.unboundImplicits : ElabDirectives -> Bool
  Totality: total
  Visibility: public export
unboundImplicits : ElabDirectives -> Bool
  Totality: total
  Visibility: public export
.totality : ElabDirectives -> TotalReq
  Totality: total
  Visibility: public export
totality : ElabDirectives -> TotalReq
  Totality: total
  Visibility: public export
.ambigLimit : ElabDirectives -> Nat
  Totality: total
  Visibility: public export
ambigLimit : ElabDirectives -> Nat
  Totality: total
  Visibility: public export
.autoImplicitLimit : ElabDirectives -> Nat
  Totality: total
  Visibility: public export
autoImplicitLimit : ElabDirectives -> Nat
  Totality: total
  Visibility: public export
.nfThreshold : ElabDirectives -> Nat
  Totality: total
  Visibility: public export
nfThreshold : ElabDirectives -> Nat
  Totality: total
  Visibility: public export
.totalLimit : ElabDirectives -> Nat
  Totality: total
  Visibility: public export
totalLimit : ElabDirectives -> Nat
  Totality: total
  Visibility: public export
.prefixRecordProjections : ElabDirectives -> Bool
  Totality: total
  Visibility: public export
prefixRecordProjections : ElabDirectives -> Bool
  Totality: total
  Visibility: public export
record PostSession : Type
  Options relevant after running a typechecking session

  Totality: total
  Visibility: public export
  Constructor: 
MkPostSession : Bool -> Maybe String -> List String -> Maybe String -> PostSession

  Projections:
  
.checkOnly : PostSession -> Bool
  
.execExpr : PostSession -> List String
  
.outputFile : PostSession -> Maybe String
  
.runRepl : PostSession -> Maybe String
.checkOnly : PostSession -> Bool
  Totality: total
  Visibility: public export
checkOnly : PostSession -> Bool
  Totality: total
  Visibility: public export
.outputFile : PostSession -> Maybe String
  Totality: total
  Visibility: public export
outputFile : PostSession -> Maybe String
  Totality: total
  Visibility: public export
.execExpr : PostSession -> List String
  Totality: total
  Visibility: public export
execExpr : PostSession -> List String
  Totality: total
  Visibility: public export
.runRepl : PostSession -> Maybe String
  Totality: total
  Visibility: public export
runRepl : PostSession -> Maybe String
  Totality: total
  Visibility: public export
defaultPost : PostSession
  Totality: total
  Visibility: export
data PostS : Type
  Totality: total
  Visibility: export
record Session : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkSessionOpts : Bool -> TotalReq -> Bool -> Bool -> CG -> List String -> Integer -> Bool -> Bool -> LogLevels -> Maybe Nat -> Bool -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Bool -> Nat -> Bool -> Bool -> Bool -> Bool -> List CG -> Bool -> Bool -> Session

  Projections:
  
.caseTreeHeuristics : Session -> Bool
  
.checkHashesInsteadOfModTime : Session -> Bool
  
.codegen : Session -> CG
  
.debugElabCheck : Session -> Bool
  
.directives : Session -> List String
  
.dumpanf : Session -> Maybe String
  
.dumpcases : Session -> Maybe String
  
.dumplifted : Session -> Maybe String
  
.dumpvmcode : Session -> Maybe String
  
.findipkg : Session -> Bool
  
.ignoreMissingPkg : Session -> Bool
  
.incrementalCGs : Session -> List CG
  
.logEnabled : Session -> Bool
  
.logErrorCount : Session -> Nat
  
.logLevel : Session -> LogLevels
  
.logTimings : Session -> Maybe Nat
  
.noCSE : Session -> Bool
  
.nobanner : Session -> Bool
  
.noprelude : Session -> Bool
  
.profile : Session -> Bool
  
.searchTimeout : Session -> Integer
  
.showShadowingWarning : Session -> Bool
  
.totalReq : Session -> TotalReq
  
.warningsAsErrors : Session -> Bool
  
.wholeProgram : Session -> Bool
.noprelude : Session -> Bool
  Totality: total
  Visibility: public export
noprelude : Session -> Bool
  Totality: total
  Visibility: public export
.totalReq : Session -> TotalReq
  Totality: total
  Visibility: public export
totalReq : Session -> TotalReq
  Totality: total
  Visibility: public export
.nobanner : Session -> Bool
  Totality: total
  Visibility: public export
nobanner : Session -> Bool
  Totality: total
  Visibility: public export
.findipkg : Session -> Bool
  Totality: total
  Visibility: public export
findipkg : Session -> Bool
  Totality: total
  Visibility: public export
.codegen : Session -> CG
  Totality: total
  Visibility: public export
codegen : Session -> CG
  Totality: total
  Visibility: public export
.directives : Session -> List String
  Totality: total
  Visibility: public export
directives : Session -> List String
  Totality: total
  Visibility: public export
.searchTimeout : Session -> Integer
  Totality: total
  Visibility: public export
searchTimeout : Session -> Integer
  Totality: total
  Visibility: public export
.ignoreMissingPkg : Session -> Bool
  Totality: total
  Visibility: public export
ignoreMissingPkg : Session -> Bool
  Totality: total
  Visibility: public export
.logEnabled : Session -> Bool
  Totality: total
  Visibility: public export
logEnabled : Session -> Bool
  Totality: total
  Visibility: public export
.logLevel : Session -> LogLevels
  Totality: total
  Visibility: public export
logLevel : Session -> LogLevels
  Totality: total
  Visibility: public export
.logTimings : Session -> Maybe Nat
  Totality: total
  Visibility: public export
logTimings : Session -> Maybe Nat
  Totality: total
  Visibility: public export
.debugElabCheck : Session -> Bool
  Totality: total
  Visibility: public export
debugElabCheck : Session -> Bool
  Totality: total
  Visibility: public export
.dumpcases : Session -> Maybe String
  Totality: total
  Visibility: public export
dumpcases : Session -> Maybe String
  Totality: total
  Visibility: public export
.dumplifted : Session -> Maybe String
  Totality: total
  Visibility: public export
dumplifted : Session -> Maybe String
  Totality: total
  Visibility: public export
.dumpanf : Session -> Maybe String
  Totality: total
  Visibility: public export
dumpanf : Session -> Maybe String
  Totality: total
  Visibility: public export
.dumpvmcode : Session -> Maybe String
  Totality: total
  Visibility: public export
dumpvmcode : Session -> Maybe String
  Totality: total
  Visibility: public export
.profile : Session -> Bool
  Totality: total
  Visibility: public export
profile : Session -> Bool
  Totality: total
  Visibility: public export
.logErrorCount : Session -> Nat
  Totality: total
  Visibility: public export
logErrorCount : Session -> Nat
  Totality: total
  Visibility: public export
.noCSE : Session -> Bool
  Totality: total
  Visibility: public export
noCSE : Session -> Bool
  Totality: total
  Visibility: public export
.warningsAsErrors : Session -> Bool
  Totality: total
  Visibility: public export
warningsAsErrors : Session -> Bool
  Totality: total
  Visibility: public export
.showShadowingWarning : Session -> Bool
  Totality: total
  Visibility: public export
showShadowingWarning : Session -> Bool
  Totality: total
  Visibility: public export
.checkHashesInsteadOfModTime : Session -> Bool
  Totality: total
  Visibility: public export
checkHashesInsteadOfModTime : Session -> Bool
  Totality: total
  Visibility: public export
.incrementalCGs : Session -> List CG
  Totality: total
  Visibility: public export
incrementalCGs : Session -> List CG
  Totality: total
  Visibility: public export
.wholeProgram : Session -> Bool
  Totality: total
  Visibility: public export
wholeProgram : Session -> Bool
  Totality: total
  Visibility: public export
.caseTreeHeuristics : Session -> Bool
  Totality: total
  Visibility: public export
caseTreeHeuristics : Session -> Bool
  Totality: total
  Visibility: public export
record PPrinter : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkPPOpts : Bool -> Bool -> Bool -> Bool -> PPrinter

  Projections:
  
.fullNamespace : PPrinter -> Bool
  
.showFullEnv : PPrinter -> Bool
  
.showImplicits : PPrinter -> Bool
  
.showMachineNames : PPrinter -> Bool
.showImplicits : PPrinter -> Bool
  Totality: total
  Visibility: public export
showImplicits : PPrinter -> Bool
  Totality: total
  Visibility: public export
.showMachineNames : PPrinter -> Bool
  Totality: total
  Visibility: public export
showMachineNames : PPrinter -> Bool
  Totality: total
  Visibility: public export
.showFullEnv : PPrinter -> Bool
  Totality: total
  Visibility: public export
showFullEnv : PPrinter -> Bool
  Totality: total
  Visibility: public export
.fullNamespace : PPrinter -> Bool
  Totality: total
  Visibility: public export
fullNamespace : PPrinter -> Bool
  Totality: total
  Visibility: public export
record Options : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkOptions : Dirs -> PPrinter -> Session -> ElabDirectives -> Maybe PairNames -> Maybe RewriteNames -> PrimNames -> List LangExt -> List (String, CG) -> Maybe String -> List (Name, String) -> Options

  Projections:
  
.additionalCGs : Options -> List (String, CG)
  
.dirs : Options -> Dirs
  
.elabDirectives : Options -> ElabDirectives
  
.extensions : Options -> List LangExt
  
.foreignImpl : Options -> List (Name, String)
  
.hashFn : Options -> Maybe String
  
.pairnames : Options -> Maybe PairNames
  
.primnames : Options -> PrimNames
  
.printing : Options -> PPrinter
  
.rewritenames : Options -> Maybe RewriteNames
  
.session : Options -> Session
.dirs : Options -> Dirs
  Totality: total
  Visibility: public export
dirs : Options -> Dirs
  Totality: total
  Visibility: public export
.printing : Options -> PPrinter
  Totality: total
  Visibility: public export
printing : Options -> PPrinter
  Totality: total
  Visibility: public export
.session : Options -> Session
  Totality: total
  Visibility: public export
session : Options -> Session
  Totality: total
  Visibility: public export
.elabDirectives : Options -> ElabDirectives
  Totality: total
  Visibility: public export
elabDirectives : Options -> ElabDirectives
  Totality: total
  Visibility: public export
.pairnames : Options -> Maybe PairNames
  Totality: total
  Visibility: public export
pairnames : Options -> Maybe PairNames
  Totality: total
  Visibility: public export
.rewritenames : Options -> Maybe RewriteNames
  Totality: total
  Visibility: public export
rewritenames : Options -> Maybe RewriteNames
  Totality: total
  Visibility: public export
.primnames : Options -> PrimNames
  Totality: total
  Visibility: public export
primnames : Options -> PrimNames
  Totality: total
  Visibility: public export
.extensions : Options -> List LangExt
  Totality: total
  Visibility: public export
extensions : Options -> List LangExt
  Totality: total
  Visibility: public export
.additionalCGs : Options -> List (String, CG)
  Totality: total
  Visibility: public export
additionalCGs : Options -> List (String, CG)
  Totality: total
  Visibility: public export
.hashFn : Options -> Maybe String
  Totality: total
  Visibility: public export
hashFn : Options -> Maybe String
  Totality: total
  Visibility: public export
.foreignImpl : Options -> List (Name, String)
  Totality: total
  Visibility: public export
foreignImpl : Options -> List (Name, String)
  Totality: total
  Visibility: public export
availableCGs : Options -> List (String, CG)
  Totality: total
  Visibility: export
getCG : Options -> String -> Maybe CG
  Totality: total
  Visibility: export
docsPPrint : PPrinter
  Totality: total
  Visibility: export
defaultSession : Session
  Totality: total
  Visibility: export
defaultElab : ElabDirectives
  Totality: total
  Visibility: export
defaultHashFn : Core (Maybe String)
  Totality: total
  Visibility: export
defaults : Core Options
  Totality: total
  Visibility: export
clearNames : Options -> Options
  Totality: total
  Visibility: export
addForeignImpl : Name -> String -> Options -> Options
  Totality: total
  Visibility: export
setPair : Name -> Name -> Name -> Options -> Options
  Totality: total
  Visibility: export
setRewrite : Name -> Name -> Options -> Options
  Totality: total
  Visibility: export
setFromInteger : Name -> Options -> Options
  Totality: total
  Visibility: export
setFromString : Name -> Options -> Options
  Totality: total
  Visibility: export
setFromChar : Name -> Options -> Options
  Totality: total
  Visibility: export
setFromDouble : Name -> Options -> Options
  Totality: total
  Visibility: export
setFromTTImp : Name -> Options -> Options
  Totality: total
  Visibility: export
setFromName : Name -> Options -> Options
  Totality: total
  Visibility: export
setFromDecls : Name -> Options -> Options
  Totality: total
  Visibility: export
setExtension : LangExt -> Options -> Options
  Totality: total
  Visibility: export
isExtension : LangExt -> Options -> Bool
  Totality: total
  Visibility: export
addCG : (String, CG) -> Options -> Options
  Totality: total
  Visibility: export