Commit 1c58bc9e authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Start working on deep inductive structures for the 'mu' combinator

parent da54796f
......@@ -542,9 +542,13 @@ mu_type (inc_depth 1 -> root_type) = yb maybeT $ go 0 root_type
]))
return $ Cons (Ap (Sym i) $ xs+[lastE])
go_col' d' _ (Universe u) = do
go_col' d' recs (Universe u) = do
let tIH = bind Prod (adjust_telescope_depth second (+(d+d')) root_args) ihRoot
ihRoot = Cons (Ap (Sym (nargs-d-1)) [Cons (Ap (Sym (j+nargs)) []) | j <- reverse [0..d'-1]])
ihRoot = Cons (Ap (Sym (nargs-d-1)) [Cons $ Ap (Sym (j+nargs)) $
if j `isKeyIn` recs
then [Cons (Ap (Sym k) []) | k <- reverse [0..nargs-1]]
else []
| j <- reverse $ select (not . (`isKeyIn`recs) . (+1)) [0..d'-1]])
return $ Bind Prod xn tIH (Universe (u+1))
go_col' _ _ _ = zero
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment