Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit 6d0b2858 authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Correct the behavior `type_of` function, causing it to fail on ill-typed terms...

Correct the behavior `type_of` function, causing it to fail on ill-typed terms instead of falsely succeeding

It was useful for debugging, though...
parent 4fd8103f
......@@ -2,7 +2,7 @@
-- see http://haskell.org/cabal/users-guide/
name: capricon
version: 0.12.2.1
version: 0.12.3
-- synopsis:
-- description:
license: GPL-3
......
......@@ -154,7 +154,7 @@ runWordsState ws st = ($st) $ from (stateT.concatT) $^ do
runWithFS :: JS.JSString -> FSIO a -> JS.CIO a
runWithFS fsname (FSIO r) = newFS fsname >>= r^..readerT
hasteDict = cocDict ("0.12.2.1-js" :: String) getString getBytes setString setBytes
hasteDict = cocDict ("0.12.3-js" :: String) getString getBytes setString setBytes
main :: IO ()
main = do
......
......@@ -530,7 +530,10 @@ type_of = yb maybeT . go
rec_subst subs (subst (Cons a') preret)
go' (Ap (Axiom t _) subs) = rec_subst subs t
rec_subst (y:t) (Bind Prod _ _ e) = rec_subst t (subst y e)
rec_subst (y:t) (Bind Prod _ tx e) = do
ty <- go y
_ <- return (convertible tx ty)^.maybeT
rec_subst t (subst y e)
rec_subst [] x = return x
rec_subst _ _ = 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