Skip to content
Permalink
Browse files

extrinsic erasure

  • Loading branch information
jmchapman committed Jan 14, 2020
1 parent ef2a342 commit a701b4bfcf8cd3ea1c8c71f0d1765d5981c26af8
Showing with 1 addition and 1 deletion.
  1. +1 −1 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

0 comments on commit a701b4b

Please sign in to comment.
You can’t perform that action at this time.