mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
More comments to illustrate how projections and type applications
are supposed to interact.
This commit is contained in:
parent
5f269dd628
commit
6734400706
@ -299,6 +299,15 @@ mkEApp es@(eLast :| _) =
|
||||
[ f, x, `{ a = 2 }, y ]
|
||||
becomes
|
||||
[ f, x ` { a = 2 }, y ]
|
||||
|
||||
The parser associates field and tuple projectors that follow an
|
||||
explicit type application onto the TTyApp term, so we also
|
||||
have to unwind those projections and reapply them. For example:
|
||||
|
||||
[ f, x, `{ a = 2 }.f.2, y ]
|
||||
becomes
|
||||
[ f, (x`{ a = 2 }).f.2, y ]
|
||||
|
||||
-}
|
||||
cvtTypeParams e [] = pure (e :| [])
|
||||
cvtTypeParams e (p : ps) =
|
||||
|
Loading…
Reference in New Issue
Block a user