@@ -48,17 +48,21 @@ elabType info syn fc opts n ty' = {- let ty' = piBind (params info) ty_in
48 let ty = addImpl i ty'
48 let ty = addImpl i ty'
49 logLvl 3 $ show n ++ " pre-type " ++ showImp True ty'
49 logLvl 3 $ show n ++ " pre-type " ++ showImp True ty'
50 logLvl 2 $ show n ++ " type " ++ showImp True ty
50 logLvl 2 $ show n ++ " type " ++ showImp True ty
51− ((ty', defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) []
51+ ((tyT, defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) []
52 (erun fc (build i info False n ty))
52 (erun fc (build i info False n ty))
53+ ds <- checkDef fc defer
55+ mapM_ (elabCaseBlock info) is
53− (cty, _) <- recheckC ctxt fc [] ty'
57+ (cty, _) <- recheckC ctxt fc [] tyT
54 logLvl 2 $ "---> " ++ show cty
59 logLvl 2 $ "---> " ++ show cty
55 let nty = normalise ctxt [] cty
60 let nty = normalise ctxt [] cty
56− ds <- checkDef fc ((n, nty):defer)
61+ ds <- checkDef fc [(n, nty)]
57 addIBC (IBCDef n)
62 addIBC (IBCDef n)
58 addDeferred ds
63 addDeferred ds
59 setFlags n opts
64 setFlags n opts
60 addIBC (IBCFlags n opts)
65 addIBC (IBCFlags n opts)
61− mapM_ (elabCaseBlock info) is
63elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()
67elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()
64elabData info syn fc (PDatadecl n t_in dcons)
68elabData info syn fc (PDatadecl n t_in dcons)