on master help sign in
Allow records in mutual blocks
4be67f7Edwin Brady
src/Idris/ElabDecls.hs+4−1
@@ -1535,9 +1535,12 @@ elabDecl' what info (PInstance s f cs n ps t expn ds)
1535 = do iLOG $ "Elaborating instance " ++ show n
1535 = do iLOG $ "Elaborating instance " ++ show n
1536 elabInstance info s f cs n ps t expn ds
1536 elabInstance info s f cs n ps t expn ds
1537elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)
1537elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)
1538− | what /= EDefns
1538+ | what /= ETypes
1539 = do iLOG $ "Elaborating record " ++ show tyn
1539 = do iLOG $ "Elaborating record " ++ show tyn
1540 elabRecord info s doc f tyn ty cdoc cn cty
1540 elabRecord info s doc f tyn ty cdoc cn cty
1541+ | otherwise
1542+ = do iLOG $ "Elaborating [type of] " ++ show tyn
1543+ elabData info s doc f False (PLaterdecl tyn ty)
1541elabDecl' _ info (PDSL n dsl)
1544elabDecl' _ info (PDSL n dsl)
1542 = do i <- getIState
1545 = do i <- getIState
1543 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })
1546 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })