TTImp.ProcessDef

Definitions

impossibleOK : Ref Ctxt Defs => Defs -> NF vars -> NF vars -> Core Bool

Visibility: export

impossibleErrOK : Ref Ctxt Defs => Defs -> Error -> Core Bool

Visibility: export

checkLHS : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => Bool -> RigCount -> Int -> List ElabOpt -> NestedNames vars -> Env Term vars -> FC -> RawImp -> Core (RawImp, (vars' : List Name ** (Thin vars vars', (Env Term vars', (NestedNames vars', (Term vars', Term vars'))))))

Visibility: export

checkClause : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => RigCount -> Visibility -> TotalReq -> Bool -> Int -> List ElabOpt -> NestedNames vars -> Env Term vars -> ImpClause -> Core (Either RawImp Clause)

Visibility: export

processDef : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => List ElabOpt -> NestedNames vars -> Env Term vars -> FC -> Name -> List ImpClause -> Core ()

Visibility: export