git.iko.soy/Idris-dev
on master help sign in
Support for inductive-inductive types
674eb4cEdwin Brady
CHANGELOG+2
compare with master
unifiedsplit
@@ -1,5 +1,7 @@
1New in 0.9.16:
1New in 0.9.16:
2--------------
2--------------
3+* Inductive-inductive definitions are now supported (i.e. simultaneously
4+ defined types where one is indexed by the other.)
3* A new tactic sourceLocation that fills the current hole with the current
5* A new tactic sourceLocation that fills the current hole with the current
4 source code span, if this information is available. If not, it raises an
6 source code span, if this information is available. If not, it raises an
5 error.
7 error.
src/Idris/Elab/Data.hs+4
@@ -227,6 +227,10 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
227 logLvl 5 $ "Inaccessible args: " ++ show inacc
227 logLvl 5 $ "Inaccessible args: " ++ show inacc
228 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'
228 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'
229
229
230+ -- Add to the context (this is temporary, so that later constructors
231+ -- can be indexed by it)
232+ updateContext (addTyDecl n (DCon 0 0 False) cty)
233+
230 addIBC (IBCDef n)
234 addIBC (IBCDef n)
231 checkDocs fc argDocs t
235 checkDocs fc argDocs t
232 doc' <- elabDocTerms info doc
236 doc' <- elabDocTerms info doc