Commit 418f13f4 authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Successful build (on Tue Apr 30 17:54:55 CEST 2019)

parent da091a1b
......@@ -534,7 +534,7 @@ type_of = yb maybeT . go
go' (Ap (Mu env _ a') subs) = do
ta <- local (map (\(x,tx,_) -> (x,tx)) env +) (go' a')
preret <- maybeT $^ mu_type $ foldl' (\e (x,tx,_) -> Bind Prod x tx e) ta env
rec_subst subs (subst (Cons a') preret)
rec_subst subs (subst (foldl' (\e (x,tx,_) -> Bind Lambda x tx e) (Cons a') env) preret)
go' (Ap (Axiom t _) subs) = rec_subst subs t
rec_subst (y:t) (Bind Prod _ tx e) = do
......
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