文件名称：STLC:相依类型的算法M和朋友
文件大小：28KB
文件格式：ZIP
更新时间：2024-06-04 13:20:43
Agda
阿格达STLC 快速品尝 从纯lambda项获取Universe多态Agda函数： phoenix : Syntax⁽⁾ phoenix = 4 # λ a b c d → a · (b · d) · (c · d) phoenixᵗ : Term ((b ⇒ c ⇒ d) ⇒ (a ⇒ b) ⇒ (a ⇒ c) ⇒ a ⇒ d) phoenixᵗ = term⁻ phoenix liftM2 : ∀ {α β γ δ} {A : Set α} {B : Set β} {C : Set γ} {D : Set δ} -> ((B -> C -> D) -> (A -> B) -> (A -> C) -> A -> D) liftM2 = eval phoenixᵗ Cc Cn liftM2给出λ {.α} {.β} {.γ} {.δ} {.A} {.B} {.C} {.D