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

Lift ! notation out of record updates

Browse Source 
It's not a block, so should be lifted
This commit is contained in:
Edwin Brady 2020-02-01 13:05:11 +00:00
parent f3cb5a8648
commit 0612bbc1ca
1 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/Idris/Desugar.idr
View File

@ -330,14 +330,15 @@ mutual
= pure $ IUnifyLog fc !(desugarB side ps tm)
desugarUpdate : {auto s : Ref Syn SyntaxInfo} ->
{auto b : Ref Bang BangData} ->
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto m : Ref MD Metadata} ->
Side -> List Name -> PFieldUpdate -> Core IFieldUpdate
desugarUpdate side ps (PSetField p v)
= pure (ISetField p !(desugar side ps v))
= pure (ISetField p !(desugarB side ps v))
desugarUpdate side ps (PSetFieldApp p v)
= pure (ISetFieldApp p !(desugar side ps v))
= pure (ISetFieldApp p !(desugarB side ps v))
expandList : {auto s : Ref Syn SyntaxInfo} ->
{auto c : Ref Ctxt Defs} ->