@@ -683,10 +683,6 @@ process h fn (NewDefn decls) = do
683 getClauseName (PClause fc name whole with rhs whereBlock) = name
683 getClauseName (PClause fc name whole with rhs whereBlock) = name
684 getClauseName (PWith fc name whole with rhs whereBlock) = name
684 getClauseName (PWith fc name whole with rhs whereBlock) = name
685 defineName :: [PDecl] -> Idris ()
685 defineName :: [PDecl] -> Idris ()
686− defineName (tyDecl@(PTy docs argdocs syn fc opts name ty) : decls) = do
687− elabDecl EAll toplevel tyDecl
688− elabClauses toplevel fc opts name (concatMap getClauses decls)
689− setReplDefined (Just name)
690 defineName [PClauses fc opts _ [clause]] = do
686 defineName [PClauses fc opts _ [clause]] = do
691 let pterm = getRHS clause
687 let pterm = getRHS clause
692 (tm,ty) <- elabVal toplevel ERHS pterm
688 (tm,ty) <- elabVal toplevel ERHS pterm