TTImp.Elab.Binders

Definitions

dropName : Name -> NestedNames vars -> NestedNames vars

Visibility: export

checkPi : 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 -> FC -> RigCount -> PiInfo RawImp -> Name -> RawImp -> RawImp -> Maybe (Glued vars) -> Core (Term vars, Glued vars)

Visibility: export

checkLambda : 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 -> FC -> RigCount -> PiInfo RawImp -> Name -> RawImp -> RawImp -> Maybe (Glued vars) -> Core (Term vars, Glued vars)

Visibility: export

checkLet : 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 -> FC -> FC -> RigCount -> Name -> RawImp -> RawImp -> RawImp -> Maybe (Glued vars) -> Core (Term vars, Glued vars)

Visibility: export