Commit dfb32c1a authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Successful build (on Sun Jan 6 14:57:38 CET 2019)

parent 17ed65ef
......@@ -542,9 +542,9 @@ 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)) []) | j <- reverse $ select (not . (`isKeyIn`recs)) [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