@@ -670,6 +670,7 @@ process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++
670 getName :: PDecl -> Maybe Name
670 getName :: PDecl -> Maybe Name
671 getName (PTy docs argdocs syn fc opts name ty) = Just name
671 getName (PTy docs argdocs syn fc opts name ty) = Just name
672 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)
672 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)
673+ getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl)
673 getName _ = Nothing
674 getName _ = Nothing
674 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes
675 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes
675 getClauseName (PClause fc name whole with rhs whereBlock) = name
676 getClauseName (PClause fc name whole with rhs whereBlock) = name
@@ -685,6 +686,8 @@ process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++
685 let tm' = force (normaliseAll ctxt [] tm)
686 let tm' = force (normaliseAll ctxt [] tm)
686 let ty' = force (normaliseAll ctxt [] ty)
687 let ty' = force (normaliseAll ctxt [] ty)
687 updateContext (addCtxtDef (getClauseName clause) (Function ty' tm'))
688 updateContext (addCtxtDef (getClauseName clause) (Function ty' tm'))
689+ defineName [PData doc argdocs syn fc opts decl] = do
690+ elabData toplevel syn doc argdocs fc opts decl
688 getClauses (PClauses fc opts name clauses) = clauses
691 getClauses (PClauses fc opts name clauses) = clauses
689 getClauses _ = []
692 getClauses _ = []
690 getRHS :: PClause -> PTerm
693 getRHS :: PClause -> PTerm