rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

𝒰 → ★

Browse source
This commit is contained in:
rhiannon morris 2022-05-09 04:30:37 +02:00
parent 50a2ec02cb
commit 5b1dab24f2
1 changed files with 14 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
tests/Tests/Equal.idr
View file

@ -52,17 +52,17 @@ export
tests : Test tests : Test
tests = "equality & subtyping" :- [ tests = "equality & subtyping" :- [
"universes" :- [ "universes" :- [
testEq "𝒰₀ ≡ 𝒰₀" $ testEq "★₀ ≡ ★₀" $
equalT (TYPE 0) (TYPE 0), equalT (TYPE 0) (TYPE 0),
testNeq "𝒰₀ ≢ 𝒰₁" $ testNeq "★₀ ≢ ★₁" $
equalT (TYPE 0) (TYPE 1), equalT (TYPE 0) (TYPE 1),
testNeq "𝒰₁ ≢ 𝒰₀" $ testNeq "★₁ ≢ ★₀" $
equalT (TYPE 1) (TYPE 0), equalT (TYPE 1) (TYPE 0),
testEq "𝒰₀ <: 𝒰₀" $ testEq "★₀ <: ★₀" $
subT (TYPE 0) (TYPE 0), subT (TYPE 0) (TYPE 0),
testEq "𝒰₀ <: 𝒰₁" $ testEq "★₀ <: ★₁" $
subT (TYPE 0) (TYPE 1), subT (TYPE 0) (TYPE 1),
testNeq "𝒰₁ ≮: 𝒰₀" $ testNeq "★₁ ≮: ★₀" $
subT (TYPE 1) (TYPE 0) subT (TYPE 1) (TYPE 0)
], ],
@ -82,29 +82,29 @@ tests = "equality & subtyping" :- [
let tm1 = Arr Zero (FT "A") (FT "B") let tm1 = Arr Zero (FT "A") (FT "B")
tm2 = Arr One (FT "A") (FT "B") in tm2 = Arr One (FT "A") (FT "B") in
subT tm1 tm2, subT tm1 tm2,
testEq "𝒰₀ ⇾ 𝒰₀ ≡ 𝒰₀ ⇾ 𝒰₀" $ testEq "★₀ ⇾ ★₀ ≡ ★₀ ⇾ ★₀" $
let tm = Arr Zero (TYPE 0) (TYPE 0) in let tm = Arr Zero (TYPE 0) (TYPE 0) in
equalT tm tm, equalT tm tm,
testEq "𝒰₀ ⇾ 𝒰₀ <: 𝒰₀ ⇾ 𝒰₀" $ testEq "★₀ ⇾ ★₀ <: ★₀ ⇾ ★₀" $
let tm = Arr Zero (TYPE 0) (TYPE 0) in let tm = Arr Zero (TYPE 0) (TYPE 0) in
subT tm tm, subT tm tm,
testNeq "𝒰₁ ⊸ 𝒰₀ ≢ 𝒰₀ ⇾ 𝒰₀" $ testNeq "★₁ ⊸ ★₀ ≢ ★₀ ⇾ ★₀" $
let tm1 = Arr Zero (TYPE 1) (TYPE 0) let tm1 = Arr Zero (TYPE 1) (TYPE 0)
tm2 = Arr Zero (TYPE 0) (TYPE 0) in tm2 = Arr Zero (TYPE 0) (TYPE 0) in
equalT tm1 tm2, equalT tm1 tm2,
testEq "𝒰₁ ⊸ 𝒰₀ <: 𝒰₀ ⊸ 𝒰₀" $ testEq "★₁ ⊸ ★₀ <: ★₀ ⊸ ★₀" $
let tm1 = Arr One (TYPE 1) (TYPE 0) let tm1 = Arr One (TYPE 1) (TYPE 0)
tm2 = Arr One (TYPE 0) (TYPE 0) in tm2 = Arr One (TYPE 0) (TYPE 0) in
subT tm1 tm2, subT tm1 tm2,
testNeq "𝒰₀ ⊸ 𝒰₀ ≢ 𝒰₀ ⇾ 𝒰₁" $ testNeq "★₀ ⊸ ★₀ ≢ ★₀ ⇾ ★₁" $
let tm1 = Arr Zero (TYPE 0) (TYPE 0) let tm1 = Arr Zero (TYPE 0) (TYPE 0)
tm2 = Arr Zero (TYPE 0) (TYPE 1) in tm2 = Arr Zero (TYPE 0) (TYPE 1) in
equalT tm1 tm2, equalT tm1 tm2,
testEq "𝒰₀ ⊸ 𝒰₀ <: 𝒰₀ ⊸ 𝒰₁" $ testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $
let tm1 = Arr One (TYPE 0) (TYPE 0) let tm1 = Arr One (TYPE 0) (TYPE 0)
tm2 = Arr One (TYPE 0) (TYPE 1) in tm2 = Arr One (TYPE 0) (TYPE 1) in
subT tm1 tm2, subT tm1 tm2,
testEq "𝒰₀ ⊸ 𝒰₀ <: 𝒰₀ ⊸ 𝒰₁" $ testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $
let tm1 = Arr One (TYPE 0) (TYPE 0) let tm1 = Arr One (TYPE 0) (TYPE 0)
tm2 = Arr One (TYPE 0) (TYPE 1) in tm2 = Arr One (TYPE 0) (TYPE 1) in
subT tm1 tm2 subT tm1 tm2
@ -170,7 +170,7 @@ tests = "equality & subtyping" :- [
todo "elim d-closure", todo "elim d-closure",
"clashes" :- [ "clashes" :- [
testNeq "𝒰₀ ≢ 𝒰₀ ⇾ 𝒰₀" $ testNeq "★₀ ≢ ★₀ ⇾ ★₀" $
equalT (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)), equalT (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)),
todo "others" todo "others"
] ]