Skip to content
Permalink
Browse files

trivial

  • Loading branch information...
jmchapman committed Mar 14, 2019
1 parent 7a00e52 commit 4a7f2426b5418d382003e19ecb52ffc5ebd5f712
Showing with 0 additions and 1 deletion.
  1. +0 −1 Scoped/Reduction.lagda
@@ -22,7 +22,6 @@ data Error {n} : ScopedTm n → Set where
E-· : {L M : ScopedTm n} → Error L → Error (L · M)
data _—→_ {n} : ScopedTm n → ScopedTm n → Set where
ξ-· : {L L' M : ScopedTm n} → L —→ L' → L · M —→ L' · M
β-· : {L L' M : ScopedTm (suc n)}
\end{code}

\begin{code}

0 comments on commit 4a7f242

Please sign in to comment.
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.