A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://github.com/agda/agda/issues/6292 below:

Document interaction between reflection and erasure · Issue #6292 · agda/agda · GitHub

The user manual section about run-time irrelevance currently does not cover reflection. I think we should specify when the reflection machinery makes the type-checker enter or leave compile-time mode.

@jespercockx, perhaps you have the best understanding of this part of the implementation. Can you write something?

I labelled this as a bug, because what is currently in the user manual is presumably not quite correct.


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