TTImp.Elab.App

Definitions

findNamed : Name -> List (Name, a) -> Maybe ((Name, a), List (Name, a))

Visibility: export

findBindAllExpPattern : List (Name, RawImp) -> Maybe RawImp

Visibility: export

checkApp : 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 -> RawImp -> List RawImp -> List RawImp -> List (Name, RawImp) -> Maybe (Glued vars) -> Core (Term vars, Glued vars)

Visibility: export