Idris.Elab.Implementation

Definitions

mkImplName : FC -> Name -> List RawImp -> Name

Visibility: export

elabImplementation : Ref Ctxt Defs => Ref UST UState => Ref Syn SyntaxInfo => Ref MD Metadata => Ref ROpts REPLOpts => FC -> Visibility -> List FnOpt -> Pass -> Env Term vars -> NestedNames vars -> List (AddFC (ImpParameter' RawImp)) -> List (Maybe Name, RawImp) -> Name -> List RawImp -> Bool -> Name -> List Name -> Maybe (List ImpDecl) -> Core ()

Visibility: export