mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-17 08:11:45 +03:00
Fix porting errors.
This commit is contained in:
parent
74dd653fc5
commit
394047906d
@ -189,7 +189,7 @@ mutual
|
||||
symbol "}"
|
||||
pure (Nothing, tm)
|
||||
|
||||
with_ : FileName -> IndentInfo -> Rule PTerm
|
||||
with_ : FileName -> IndentInfo -> SourceRule PTerm
|
||||
with_ fname indents
|
||||
= do start <- location
|
||||
keyword "with"
|
||||
@ -199,12 +199,12 @@ mutual
|
||||
rhs <- expr pdef fname indents
|
||||
pure (PWithUnambigNames (MkFC fname start end) ns rhs)
|
||||
where
|
||||
singleName : Rule (List Name)
|
||||
singleName : SourceRule (List Name)
|
||||
singleName = do
|
||||
n <- name
|
||||
pure [n]
|
||||
|
||||
nameList : Rule (List Name)
|
||||
nameList : SourceRule (List Name)
|
||||
nameList = do
|
||||
symbol "["
|
||||
commit
|
||||
|
@ -218,8 +218,7 @@ checkTerm rig elabinfo nest env (Implicit fc b) Nothing
|
||||
put EST (addBindIfUnsolved nm rig Explicit env metaval ty est)
|
||||
pure (metaval, gnf env ty)
|
||||
checkTerm rig elabinfo nest env (IWithUnambigNames fc ns rhs) exp
|
||||
= with Core do
|
||||
-- enter the scope -> add unambiguous names
|
||||
= do -- enter the scope -> add unambiguous names
|
||||
est <- get EST
|
||||
rns <- resolveNames fc ns
|
||||
put EST $ record { unambiguousNames = mergeLeft rns (unambiguousNames est) } est
|
||||
|
Loading…
Reference in New Issue
Block a user