Idris2Doc : TTImp.Elab.Check

TTImp.Elab.Check

(source)
Definitions
data ElabMode : Type
  Totality: total
  Visibility: public export
  Constructors:
  
InType : ElabMode
  
InLHS : RigCount -> ElabMode
  
InExpr : ElabMode
  
InTransform : ElabMode

  Hint: 
Show ElabMode
isLHS : ElabMode -> Maybe RigCount
  Visibility: export
data ElabOpt : Type
  Totality: total
  Visibility: public export
  Constructors:
  
HolesOkay : ElabOpt
  
InCase : ElabOpt
  
InPartialEval : ElabOpt
  
InTrans : ElabOpt

  Hint: 
Eq ElabOpt
data ImplBinding : Scope -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
NameBinding : FC -> RigCount -> PiInfo (Term vars) -> Term vars -> Term vars -> ImplBinding vars
  
AsBinding : RigCount -> PiInfo (Term vars) -> Term vars -> Term vars -> Term vars -> ImplBinding vars

  Hint: 
Show (ImplBinding vars)
bindingMetas : ImplBinding vars -> NameMap Bool
  Visibility: export
bindingType : ImplBinding vars -> Term vars
  Visibility: export
bindingTerm : ImplBinding vars -> Term vars
  Visibility: export
bindingRig : ImplBinding vars -> RigCount
  Visibility: export
bindingPiInfo : ImplBinding vars -> PiInfo (Term vars)
  Visibility: export
record EState : Scope -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkEState : Int -> Env Term outer -> Thin outer vars -> List (Name, ImplBinding vars) -> List (Name, ImplBinding vars) -> List (Name, (FC, (RigCount, (vars' : List Name ** (Env Term vars', (PiInfo (Term vars'), (Term vars', (Term vars', Thin outer vars')))))))) -> List Name -> List Name -> List (FC, (Env Term vars, (Term vars, Term vars))) -> Nat -> VarSet vars -> NameMap () -> UserNameMap (Name, (Int, GlobalDef)) -> EState vars

  Projections:
  
.allPatVars : EState vars -> List Name
  
.bindIfUnsolved : ({rec:0} : EState vars) -> List (Name, (FC, (RigCount, (vars' : List Name ** (Env Term vars', (PiInfo (Term vars'), (Term vars', (Term vars', Thin (outer {rec:0}) vars'))))))))
  
.boundNames : EState vars -> List (Name, ImplBinding vars)
  
.defining : EState vars -> Int
  
.delayDepth : EState vars -> Nat
  
.lhsPatVars : EState vars -> List Name
  
.linearUsed : EState vars -> VarSet vars
  
.outer : EState vars -> Scope
  
.outerEnv : ({rec:0} : EState vars) -> Env Term (outer {rec:0})
  
.polyMetavars : EState vars -> List (FC, (Env Term vars, (Term vars, Term vars)))
  
.saveHoles : EState vars -> NameMap ()
  
.subEnv : ({rec:0} : EState vars) -> Thin (outer {rec:0}) vars
  
.toBind : EState vars -> List (Name, ImplBinding vars)
  
.unambiguousNames : EState vars -> UserNameMap (Name, (Int, GlobalDef))
.outer : EState vars -> Scope
  Visibility: public export
outer : EState vars -> Scope
  Visibility: public export
.defining : EState vars -> Int
  Visibility: public export
defining : EState vars -> Int
  Visibility: public export
.outerEnv : ({rec:0} : EState vars) -> Env Term (outer {rec:0})
  Visibility: public export
outerEnv : ({rec:0} : EState vars) -> Env Term (outer {rec:0})
  Visibility: public export
.subEnv : ({rec:0} : EState vars) -> Thin (outer {rec:0}) vars
  Visibility: public export
subEnv : ({rec:0} : EState vars) -> Thin (outer {rec:0}) vars
  Visibility: public export
.boundNames : EState vars -> List (Name, ImplBinding vars)
  Visibility: public export
boundNames : EState vars -> List (Name, ImplBinding vars)
  Visibility: public export
.toBind : EState vars -> List (Name, ImplBinding vars)
  Visibility: public export
toBind : EState vars -> List (Name, ImplBinding vars)
  Visibility: public export
.bindIfUnsolved : ({rec:0} : EState vars) -> List (Name, (FC, (RigCount, (vars' : List Name ** (Env Term vars', (PiInfo (Term vars'), (Term vars', (Term vars', Thin (outer {rec:0}) vars'))))))))
  Visibility: public export
bindIfUnsolved : ({rec:0} : EState vars) -> List (Name, (FC, (RigCount, (vars' : List Name ** (Env Term vars', (PiInfo (Term vars'), (Term vars', (Term vars', Thin (outer {rec:0}) vars'))))))))
  Visibility: public export
.lhsPatVars : EState vars -> List Name
  Visibility: public export
lhsPatVars : EState vars -> List Name
  Visibility: public export
.allPatVars : EState vars -> List Name
  Visibility: public export
allPatVars : EState vars -> List Name
  Visibility: public export
.polyMetavars : EState vars -> List (FC, (Env Term vars, (Term vars, Term vars)))
  Visibility: public export
polyMetavars : EState vars -> List (FC, (Env Term vars, (Term vars, Term vars)))
  Visibility: public export
.delayDepth : EState vars -> Nat
  Visibility: public export
delayDepth : EState vars -> Nat
  Visibility: public export
.linearUsed : EState vars -> VarSet vars
  Visibility: public export
linearUsed : EState vars -> VarSet vars
  Visibility: public export
.saveHoles : EState vars -> NameMap ()
  Visibility: public export
saveHoles : EState vars -> NameMap ()
  Visibility: public export
.unambiguousNames : EState vars -> UserNameMap (Name, (Int, GlobalDef))
  Visibility: public export
unambiguousNames : EState vars -> UserNameMap (Name, (Int, GlobalDef))
  Visibility: public export
data EST : Type
  Totality: total
  Visibility: export
initEStateSub : Int -> Env Term outer -> Thin outer vars -> EState vars
  Visibility: export
initEState : Int -> Env Term vars -> EState vars
  Visibility: export
saveHole : Ref EST (EState vars) => Name -> Core ()
  Visibility: export
inScope : Ref Ctxt Defs => Ref EST (EState vars) => FC -> Env Term (n :: vars) -> (Ref EST (EState (n :: vars)) -> Core a) -> Core a
  Visibility: export
mustBePoly : Ref EST (EState vars) => FC -> Env Term vars -> Term vars -> Term vars -> Core ()
  Visibility: export
concrete : Defs -> Env Term vars -> NF vars -> Core Bool
  Visibility: export
updateEnv : Env Term new -> Thin new vars -> List (Name, (FC, (RigCount, (vars' : List Name ** (Env Term vars', (PiInfo (Term vars'), (Term vars', (Term vars', Thin new vars')))))))) -> EState vars -> EState vars
  Visibility: export
addBindIfUnsolved : Name -> FC -> RigCount -> PiInfo (Term vars) -> Env Term vars -> Term vars -> Term vars -> EState vars -> EState vars
  Visibility: export
clearToBind : Ref EST (EState vars) => List Name -> Core ()
  Visibility: export
noteLHSPatVar : Ref EST (EState vars) => ElabMode -> Name -> Core ()
  Visibility: export
notePatVar : Ref EST (EState vars) => Name -> Core ()
  Visibility: export
metaVar : Ref Ctxt Defs => Ref UST UState => FC -> RigCount -> Env Term vars -> Name -> Term vars -> Core (Term vars)
  Visibility: export
implBindVar : Ref Ctxt Defs => Ref UST UState => FC -> RigCount -> Env Term vars -> Name -> Term vars -> Core (Term vars)
  Visibility: export
metaVarI : Ref Ctxt Defs => Ref UST UState => FC -> RigCount -> Env Term vars -> Name -> Term vars -> Core (Int, Term vars)
  Visibility: export
argVar : Ref Ctxt Defs => Ref UST UState => FC -> RigCount -> Env Term vars -> Name -> Term vars -> Core (Int, Term vars)
  Visibility: export
uniVar : Ref Ctxt Defs => Ref UST UState => FC -> Core Name
  Visibility: export
searchVar : Ref Ctxt Defs => Ref UST UState => FC -> RigCount -> Nat -> Name -> Env Term vars -> NestedNames vars -> Name -> Term vars -> Core (Term vars)
  Visibility: export
record ElabInfo : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkElabInfo : ElabMode -> BindMode -> Bool -> Bool -> Bool -> List Name -> ElabInfo

  Projections:
  
.ambigTries : ElabInfo -> List Name
  
.bindingVars : ElabInfo -> Bool
  
.elabMode : ElabInfo -> ElabMode
  
.implicitMode : ElabInfo -> BindMode
  
.preciseInf : ElabInfo -> Bool
  
.topLevel : ElabInfo -> Bool
.elabMode : ElabInfo -> ElabMode
  Visibility: public export
elabMode : ElabInfo -> ElabMode
  Visibility: public export
.implicitMode : ElabInfo -> BindMode
  Visibility: public export
implicitMode : ElabInfo -> BindMode
  Visibility: public export
.topLevel : ElabInfo -> Bool
  Visibility: public export
topLevel : ElabInfo -> Bool
  Visibility: public export
.bindingVars : ElabInfo -> Bool
  Visibility: public export
bindingVars : ElabInfo -> Bool
  Visibility: public export
.preciseInf : ElabInfo -> Bool
  Visibility: public export
preciseInf : ElabInfo -> Bool
  Visibility: public export
.ambigTries : ElabInfo -> List Name
  Visibility: public export
ambigTries : ElabInfo -> List Name
  Visibility: public export
initElabInfo : ElabMode -> ElabInfo
  Visibility: export
tryError : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref EST (EState vars) => Core a -> Core (Either Error a)
  Visibility: export
try : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref EST (EState vars) => Core a -> Core a -> Core a
  Visibility: export
handle : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref EST (EState vars) => Core a -> (Error -> Core a) -> Core a
  Visibility: export
exactlyOne' : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref EST (EState vars) => Bool -> FC -> Env Term vars -> List (Maybe Name, Core (Term vars, Glued vars)) -> Core (Term vars, Glued vars)
  Visibility: export
exactlyOne : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref EST (EState vars) => FC -> Env Term vars -> List (Maybe Name, Core (Term vars, Glued vars)) -> Core (Term vars, Glued vars)
  Visibility: export
anyOne : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref EST (EState vars) => FC -> List (Maybe Name, Core (Term vars, Glued vars)) -> Core (Term vars, Glued vars)
  Visibility: export
check : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref EST (EState vars) => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => RigCount -> ElabInfo -> NestedNames vars -> Env Term vars -> RawImp -> Maybe (Glued vars) -> Core (Term vars, Glued vars)
  Visibility: export
checkImp : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref EST (EState vars) => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => RigCount -> ElabInfo -> NestedNames vars -> Env Term vars -> RawImp -> Maybe (Glued vars) -> Core (Term vars, Glued vars)
  Visibility: export
processDecl : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => List ElabOpt -> NestedNames vars -> Env Term vars -> ImpDecl -> Core ()
  Visibility: export
convert : Ref Ctxt Defs => Ref UST UState => FC -> ElabInfo -> Env Term vars -> Glued vars -> Glued vars -> Core UnifyResult
  Visibility: export
checkExp : Ref Ctxt Defs => Ref UST UState => RigCount -> ElabInfo -> Env Term vars -> FC -> Term vars -> Glued vars -> Maybe (Glued vars) -> Core (Term vars, Glued vars)
  Visibility: export