open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.String
abstract
foo : Nat → Nat
foo n = n + 5
show : Nat → String
show n = primShowNat (foo n)
test : show 0 ≡ "5"
test = {!refl!} -- As expected, the abstract def prevents this from going through
_ = {!0!} -- Bad: normalises to 5, seeing through the abstract block
When I define show for a type using a function that was defined inside an abstract block, as above, I would expect it to get stuck on the abstract function foo. And indeed, that happens in most cases, eg in test. But when show is called by Agda when I normalise the goal at the end of the above example, Agda sees through the abstract block and prints 5. The same behaviour occurs when replacing abstract by opaque.
Tested on Agda 2.6.4.
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