Since 2013 (3777ddf) Agda has support for let-bindings in telescopes, e.g. (x : Nat) (let y = x + x) (v : Vec Nat y) -> .... However as far as I can see it has never been documented in the user manual (I looked in the documentation of local definitions, function types, and modules). Curiously we do have a tag for the feature on Github (let-telescopes).
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4