extrinsic erasure

IntersectMBO · Jan 14, 2020 · a701b4b · a701b4b
1 parent ef2a342
commit a701b4b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/metatheory/Scoped/Erasure.lagda b/metatheory/Scoped/Erasure.lagda
@@ -38,7 +38,7 @@ eraseList (t ∷ ts) = eraseTm t ∷ eraseList ts
 eraseTm (` x)              = ` (eraseVar x)
 eraseTm (Λ K t)            = eraseTm t
 eraseTm (t ·⋆ A)           = eraseTm t
-eraseTm (ƛ A t)            = ƛ {!!} (eraseTm t)
+eraseTm (ƛ A t)            = ƛ (eraseTm t)
 eraseTm (t · u)            = eraseTm t · eraseTm u
 eraseTm (con c)            = con (eraseTC c)
 eraseTm (error A)          = error