Commit 70ec66b9 authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Successful build (on Sun Jan 6 15:01:38 CET 2019)

parent 416cc337
......@@ -544,7 +544,11 @@ mu_type (inc_depth 1 -> root_type) = yb maybeT $ go 0 root_type
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 $ select (not . (`isKeyIn`recs) . (+1)) [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
......
Supports Markdown
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