View on GitHub
File Changes
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