@@ -693,27 +693,6 @@ process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++
693 getRHS (PClauseR fc with rhs whereBlock) = rhs
693 getRHS (PClauseR fc with rhs whereBlock) = rhs
694 getRHS (PWithR fc with rhs whereBlock) = rhs
694 getRHS (PWithR fc with rhs whereBlock) = rhs
696−-- process h fn (NewDefn (tyDecl:decls)) | isTyDecl tyDecl = do
697−-- elabDecl EAll toplevel tyDecl
698−-- (name, fc) <- getInfo tyDecl
699−-- logLvl 3 $ "Defining " ++ show name ++ " with this type decl: " ++ show tyDecl
700−-- logLvl 5 $ "Using this definition: " ++ show decls
701−-- elabClauses toplevel fc [] name defn
702−-- where getInfo (PTy docs argdocs syn fc opts name ty) = return (name, fc)
703−-- getInfo _ = fail "New definitions must begin with a type declaration"
704−-- isTyDecl PTy{} = True
705−-- isTyDecl _ = False
706−-- defn = concatMap getClauses decls
707−-- getClauses (PClauses fc opts name clauses) = clauses
710−-- process h fn (NewDefn [PCAF fc name val])
711−-- = do (tm, ty) <- elabVal toplevel False val
712−-- ctxt <- getContext
713−-- let tm' = force (normaliseAll ctxt [] tm)
714−-- let ty' = force (normaliseAll ctxt [] ty)
715−-- updateContext (addCtxtDef name (Function ty' tm'))
717process h fn (ExecVal t)
696process h fn (ExecVal t)
718 = do ctxt <- getContext
697 = do ctxt <- getContext
719 ist <- getIState
698 ist <- getIState