edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-23 20:22:34 +03:00
Code Issues Projects Releases Wiki Activity

Bugfix: In mapPTerm, correctly handle the parameter list in a PRecord

Browse Source 
Ta @gallais !
This commit is contained in:
Ohad Kammar 2020-04-17 08:36:41 +01:00
parent 73d2e7bc29
commit c5070eba19
1 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/Idris/Syntax.idr
View File

@ -884,11 +884,12 @@ mapPTermM f = goPTerm where
(::) . (\ c => (a, b, c)) <$> goPTerm t
<*> go3TupledPTerms ts
go4TupledPTerms : List (a, b, c, PTerm) -> Core (List (a, b, c, PTerm))
go4TupledPTerms : List (a, b, PiInfo PTerm, PTerm) -> Core (List (a, b, PiInfo PTerm, PTerm))
go4TupledPTerms [] = pure []
go4TupledPTerms ((a, b, c, t) :: ts) =
(::) . (\ d => (a, b, c, d)) <$> goPTerm t
<*> go4TupledPTerms ts
go4TupledPTerms ((a, b, p, t) :: ts) =
(\ p, d, ts => (a, b, p, d) :: ts) <$> goPiInfo p
<*> goPTerm t
<*> go4TupledPTerms ts
goPDos : List PDo -> Core (List PDo)
goPDos [] = pure []