In the course of working on Indexed HITs, I've needed a notion of telescope built in to cooltt to simplify some nasty termbuilder manipulations. This also simplifies quite a bit of the signature code, so I've spun this off into it's own PR.
The major change is that Signature and CodeSignature are no longer parameterized by a list of field types, but rather a tele and kan_tele, respectively. This allows us to pull some of our elaborator hacks into Syntax, which gets handled by evaluation rather than elaboration. Note that we disallow neutral telescopes, which avoids quite a few problems involving staging.
favonia
commented
1 year ago
Description
In the course of working on Indexed HITs, I've needed a notion of telescope built in to cooltt to simplify some nasty termbuilder manipulations. This also simplifies quite a bit of the signature code, so I've spun this off into it's own PR.
The major change is that
SignatureandCodeSignatureare no longer parameterized by a list of field types, but rather ateleandkan_tele, respectively. This allows us to pull some of our elaborator hacks intoSyntax, which gets handled by evaluation rather than elaboration. Note that we disallow neutral telescopes, which avoids quite a few problems involving staging.