module Lambda.TwoSemantics where
open import Coinduction
open import Lambda.Syntax
open import Lambda.Substitution
infix 4 _⇓_
data _⇓_ {n} : Tm n → Value n → Set where
val : ∀ {v} → ⌜ v ⌝ ⇓ v
app : ∀ {t₁ t₂ t v v′}
(t₁⇓ : t₁ ⇓ ƛ t)
(t₂⇓ : t₂ ⇓ v)
(t₁t₂⇓ : t / sub ⌜ v ⌝ ⇓ v′) →
t₁ · t₂ ⇓ v′
infix 4 _⇑
data _⇑ {n} : Tm n → Set where
·ˡ : ∀ {t₁ t₂}
(t₁⇑ : ∞ (t₁ ⇑)) →
t₁ · t₂ ⇑
·ʳ : ∀ {t₁ t₂ v}
(t₁⇓ : t₁ ⇓ v)
(t₂⇑ : ∞ (t₂ ⇑)) →
t₁ · t₂ ⇑
app : ∀ {t₁ t₂ t v}
(t₁⇓ : t₁ ⇓ ƛ t)
(t₂⇓ : t₂ ⇓ v)
(t₁t₂⇓ : ∞ (t / sub ⌜ v ⌝ ⇑)) →
t₁ · t₂ ⇑