@@ -692,9 +692,12 @@ process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++
692 let ty' = force (normaliseAll ctxt [] ty)
692 let ty' = force (normaliseAll ctxt [] ty)
693 updateContext (addCtxtDef (getClauseName clause) (Function ty' tm'))
693 updateContext (addCtxtDef (getClauseName clause) (Function ty' tm'))
694 setReplDefined (Just $ getClauseName clause)
694 setReplDefined (Just $ getClauseName clause)
695− defineName [def @ (PData doc argdocs syn fc opts decl)] = do
695+ -- fixity and syntax declarations are ignored by elabDecls, so they'll have to be handled some other way
696− elabData toplevel syn doc argdocs fc opts decl
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
697− setReplDefined (getName def)
700+ setReplDefined (getName (head decls))
698 getClauses (PClauses fc opts name clauses) = clauses
701 getClauses (PClauses fc opts name clauses) = clauses
699 getClauses _ = []
702 getClauses _ = []
700 getRHS :: PClause -> PTerm
703 getRHS :: PClause -> PTerm