idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-24 20:23:11 +03:00
Code Issues Projects Releases Wiki Activity

[ re #2871 ] Fix the resolvedN issue for good

Browse Source
This commit is contained in:
Guillaume Allais 2023-02-04 14:21:04 +00:00 committed by G. Allais
parent f6a731695d
commit 21fa60ae6a
2 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/TTImp/ProcessRecord.idr
View File

@ -166,10 +166,10 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params0 opts conName_i
Core (vars' ** (Env Term vars', Term vars'))
dropLeadingPis [] ty env
= do unless (null vars) $
log "declare.record.parameters" 60 $ unlines
logC "declare.record.parameters" 60 $ pure $ unlines
[ "We elaborated \{show tn} in a non-empty local context."
, " Dropped: \{show vars}"
, " Remaining type: \{show ty}"
, " Remaining type: \{show !(toFullNames ty)}"
]
pure (_ ** (env, ty))
dropLeadingPis (var :: vars) (Bind fc n b@(Pi _ _ _ _) ty) env

2
tests/idris2/record019/expected
View File

@ -12,6 +12,6 @@ LOG declare.record.parameters:50: Decided to bind the following extra parameters
LOG declare.record.parameters:60: We elaborated Main.EtaProof in a non-empty local context.
Dropped: [b, a]
Remaining type: (p : ($resolved2702 a[1] b[0])) -> Type
Remaining type: (p : (Main.Product a[1] b[0])) -> Type
LOG declare.record.parameters:30: Unelaborated type: (%pi RigW Explicit Nothing Main.Product %type)