Introduce an `abstract` command
Closed this issue · 4 comments
Introduce a command which abstracts a judgement with respect to an atom. The syntax should be
abstract x e
Thus {x : A} c should be equivalent to
let x = fresh x : A in
let e = c in
abstract x e
Do I understand correctly from the existence of this issue that there is currently no way to do this in Andromeda 2.0? Does that mean in particular that there isn't yet any way to implement a "Hole" operation that works inside arbitrary binders, as was possible in Andromeda 1.0?
Would this follow from being able to substitute for atoms? That is, could abstract x e be defined as {y} e where x = y if the latter existed?
Yes, precisely. This is about which operations should be taken as basic. Substitution e where x = e' is expressible as (abstract x e){e'}. Conversely, abstraction is expressible as you wrote.
Closed by #473