wball/perga
1
0
Fork 0
Code Issues 15 Pull requests Projects Releases Packages Wiki Activity Actions

applied fix to other ascriptions

Browse source
This commit is contained in:
William Ball 2024-12-05 19:05:34 -08:00
parent c0e0c37689
commit 7e3a347485
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
lib/Check.hs
View file

@ -60,17 +60,18 @@ findType g e@(App m n) = do
findType g f@(Abs x a asc m) = do findType g f@(Abs x a asc m) = do
validateType g a validateType g a
b <- findType (incIndices a : map incIndices g) m b <- findType (incIndices a : map incIndices g) m
whenJust asc (betaEquiv' f b) whenJust asc (void . liftA2 ($>) (findType g) (betaEquiv' f b))
validateType g (Pi x a Nothing b) validateType g (Pi x a Nothing b)
pure $ if occursFree 0 b then Pi x a Nothing b else Pi "" a Nothing b pure $ if occursFree 0 b then Pi x a Nothing b else Pi "" a Nothing b
findType g f@(Pi _ a asc b) = do findType g f@(Pi _ a asc b) = do
aSort <- findType g a aSort <- findType g a
bSort <- findType (incIndices a : map incIndices g) b bSort <- findType (incIndices a : map incIndices g) b
whenJust asc $ betaEquiv' f bSort whenJust asc (void . liftA2 ($>) (findType g) (betaEquiv' f bSort))
liftEither $ compSort a b aSort bSort liftEither $ compSort a b aSort bSort
findType g (Let _ Nothing v b) = findType g (subst 0 v b) findType g (Let _ Nothing v b) = findType g (subst 0 v b)
findType g e@(Let _ (Just t) v b) = do findType g e@(Let _ (Just t) v b) = do
res <- findType g (subst 0 v b) res <- findType g (subst 0 v b)
_ <- findType g t
betaEquiv' e t res betaEquiv' e t res
pure t pure t