Skip to content
Permalink
Browse files

trying a different approach to reducing error for well scoped terms

  • Loading branch information...
jmchapman committed Mar 14, 2019
1 parent ad8e20f commit 7a00e5259c1fbaa60231beac55ea03afa4b3c05a
Showing with 7 additions and 7 deletions.
  1. +7 −7 Scoped/Reduction.lagda
@@ -17,12 +17,12 @@ infix 2 _—→_
data Value {n} : ScopedTm n → Set where
V-ƛ : (A : ScopedTy ∥ n ∥)(t : ScopedTm (S n)) → Value (ƛ A t)
-- V-con : (tcn : TermCon) → Value (con {n} tcn)
data Error : ∀{n} → ScopedTm n → Set where

data Error {n} : ScopedTm n → Set where
E-error : (A : ScopedTy ∥ n ∥) → Error (error A)
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
E-· : {L M : ScopedTm n} → Error L → L · M —→ error {!!}

β-· : {L L' M : ScopedTm (suc n)}
\end{code}

\begin{code}
@@ -40,10 +40,10 @@ progress (t ·⋆ A) = {!!}
progress (ƛ A t) = {!!}
progress (t · u) with progress t
progress (.(ƛ A t) · u) | inl (inl (V-ƛ A t)) = {!!}
progress (t · u) | inl (inr p) = inr ((error {!!}) , {!!})
progress (t · u) | inr y = {!!}
progress (t · u) | inl (inr p) = inl (inr (E-· p))
progress (t · u) | inr (t' , p) = inr (t' · u , ξ-· p)
progress (con x) = {!!}
progress (error x) = {!!}
progress (error p) = inl (inr (E-error p))
progress (builtin x) = {!!}
\end{code}

0 comments on commit 7a00e52

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.