You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This is a new encoding of HOLE that differentiates between type and
term arguments of the hole.
```
-- pickled quote trees: These trees can only appear in pickled quotes. They will never be in a TASTy file.
EXPLICITtpt tpt_Term
-- Tag for a type tree that in a context where it is not explicitly known that this tree is a type.
HOLE Length idx_Nat tpe_Type arg_Tree*
-- Splice hole with index `idx`, the type of the hole `tpe`, type and term arguments of the hole `arg`s
```
We will only have hole captured types if there is a type defined in a quote and used in a nested quote.
Most of the time we do not have those types and therefore no overhead in the encoding compared to before this change.
0 commit comments