View on GitHub
File Changes
-- intrinsically typed terms should also carry user chosen names as
-- instructions to the pretty printer

                      
-
extricateNf⋆ (Π {K = K} x A) = Π K (extricateNf⋆ A)
+
extricateNf⋆ (Π {K = K} A) = Π K (extricateNf⋆ A)
extricateNf⋆ (A ⇒ B) = extricateNf⋆ A ⇒ extricateNf⋆ B
-
extricateNf⋆ (ƛ {K = K} x A) = ƛ K (extricateNf⋆ A)
+
extricateNf⋆ (ƛ {K = K} A) = ƛ K (extricateNf⋆ A)
extricateNf⋆ (ne n) = extricateNe⋆ n
extricateNf⋆ (con c) = con c

                      
open import Relation.Binary.PropositionalEquality as Eq

                      
extricateVar : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *} → Γ ∋ A → WeirdFin (len Γ)
-
extricateVar (Z _) = Z
+
extricateVar Z = Z
extricateVar (S x) = S (extricateVar x)
-
extricateVar (T x _) = T (extricateVar x)
+
extricateVar (T x) = T (extricateVar x)

                      
extricateC : ∀{Γ}{A : Γ ⊢Nf⋆ *} → B.TermCon A → Scoped.TermCon
extricateC (integer i)    = integer i
extricateTel σ (A ∷ As) (t P., ts) = extricate t ∷ extricateTel σ As ts

                      
extricate (` x) = ` (extricateVar x)
-
extricate {Φ}{Γ} (ƛ {A = A} x t) = ƛ (extricateNf⋆ A) (extricate t)
+
extricate {Φ}{Γ} (ƛ {A = A} t) = ƛ (extricateNf⋆ A) (extricate t)
extricate (t · u) = extricate t · extricate u
-
extricate (Λ {K = K} x t) = Λ K (extricate t)
-
extricate {Φ}{Γ} (·⋆ t A _) = extricate t ScopedTm.·⋆ extricateNf⋆ A
+
extricate (Λ {K = K} t) = Λ K (extricate t)
+
extricate {Φ}{Γ} (_·⋆_ t A) = extricate t ScopedTm.·⋆ extricateNf⋆ A
extricate {Φ}{Γ} (wrap1 pat arg t) = wrap (extricateNf⋆ pat) (extricateNf⋆ arg)
  (extricate t)
-
extricate (unwrap1 t _) = unwrap (extricate t)
+
extricate (unwrap1 t) = unwrap (extricate t)
extricate (con c) = con (extricateC c)
-
extricate {Φ}{Γ} (builtin b σ ts _) =
+
extricate {Φ}{Γ} (builtin b σ ts) =
  builtin b (extricateSub σ) (extricateTel σ _ ts)
extricate {Φ}{Γ} (error A) = error (extricateNf⋆ A)
\end{code}