@@ -692,9 +692,12 @@ process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++
692692 let ty' = force (normaliseAll ctxt [] ty)
693693 updateContext (addCtxtDef (getClauseName clause) (Function ty' tm'))
694694 setReplDefined (Just $ getClauseName clause)
695− defineName [def @ (PData doc argdocs syn fc opts decl)] = do
696− elabData toplevel syn doc argdocs fc opts decl
697− setReplDefined (getName def)
695+ -- fixity and syntax declarations are ignored by elabDecls, so they'll have to be handled some other way
696+ defineName (PFix{}:_) = tclift $ tfail (Msg "That kind of declaration is not supported. If you feel it should be supported, please submit an issue at https://github.com/idris-lang/Idris-dev.")
697+ defineName (PSyntax{}:_) = tclift $ tfail (Msg "That kind of declaration is not supported. If you feel it should be supported, please submit an issue at https://github.com/idris-lang/Idris-dev.")
698+ defineName decls = do
699+ elabDecls toplevel decls
700+ setReplDefined (getName (head decls))
698701 getClauses (PClauses fc opts name clauses) = clauses
699702 getClauses _ = []
700703 getRHS :: PClause -> PTerm