prove complete progress
Closed this issue · 0 comments
ivoysey commented
data ok : (d : dhexp) (Δ : hctx) → Set where
V : ∀{d Δ} → d val → ok d Δ
S : ∀{d Δ} → Σ[ d' ∈ dhexp ] (Δ ⊢ d ↦ d') → ok d Δ
-- nb: don't need (Δ , ∅ ⊢ d :: τ) because of typed-expansion
complete-progress : {Δ : hctx} {d : dhexp} {τ : htyp} {e : hexp}→
ecomplete e →
∅ ⊢ e ⇒ τ ~> d ⊣ Δ →
ok d Δ
@cyrus- said one or both of these was trivial and should be removed but i forget which one