'What does it mean to erase an argument in an erased function?
When I define type synonyms I typically erase them as 0 Foo : Type. If there are parameters to that synonym, I can also erase those, like
0 Foo : (0 _ : Nat) -> (0 _ : Type) -> Type
but what does that mean? Since Foo doesn't exist at runtime, nothing it's passed needs to exist at runtime either. We can see this by defining a similar example without erased args
0 Foo' : Nat -> Type -> Type
and defining Foo in terms of Foo'
Foo x a = Foo' x a
which compiles fine. Is there any purpose to erasing arguments to erased functions?
Sources
This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.
Source: Stack Overflow
| Solution | Source |
|---|