rhi/quox
rhi
/
quox
1
0
Fork 0
Code Issues 16 Pull Requests 1 Releases Wiki Activity

misc.All doesn't need to be a ★¹

This commit is contained in:
rhiannon morris 2023-11-03 17:42:31 +01:00
parent baafa065c5
commit 6d9e4656bf
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
examples/misc.quox
View File

@ -6,7 +6,7 @@ def0 Not : ★ → ★ = λ A ⇒ ω.A → False
def void : 0.(A : ★) → 0.False → A =
λ A v ⇒ case0 v return A of { }
def0 All : (A : ★) → (0.A → ★) → ★¹ =
def0 All : (A : ★) → (0.A → ★) → ★ =
λ A P ⇒ (x : A) → P x
def0 cong :