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

rename λᴰ to δ

Browse source 
sorry fen
This commit is contained in:
rhiannon morris 2023-02-25 19:14:11 +01:00
parent 302de6266e
commit 4b284d6e01
4 changed files with 18 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
lib/Quox/Syntax/Term/Pretty.idr
View file

@ -18,7 +18,7 @@ timesD = hlF Syntax $ ifUnicode "×" "**"
darrowD = hlF Syntax $ ifUnicode "⇒" "=>"
lamD = hlF Syntax $ ifUnicode "λ" "fun"
eqndD = hlF Syntax $ ifUnicode "≡" "=="
dlamD = hlF Syntax $ ifUnicode "λᴰ" "dfun"
dlamD = hlF Syntax $ ifUnicode "δ" "dfun"
annD = hlF Syntax $ ifUnicode "∷" "::"
private %inline

2
lib/Quox/Typechecker.idr
View file

@ -174,7 +174,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
equal ctx ty.zero body.zero l
-- if Ψ | Γ ⊢ t‹1› = r : A‹1›
equal ctx ty.one body.one r
-- then Ψ | Γ ⊢ σ · (λᴰi ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ
-- then Ψ | Γ ⊢ σ · (δ i ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ
pure qout
check' ctx sg (E e) ty = do

4
tests/Tests/Equal.idr
View file

@ -169,7 +169,7 @@ tests = "equality & subtyping" :- [
refl a x = (DLam $ S ["_"] $ N x) :# (Eq0 a x x)
in
[
note #""refl [A] x" is an abbreviation for "(λᴰi ⇒ x) ∷ (x ≡ x : A)""#,
note #""refl [A] x" is an abbreviation for "(δ i ⇒ x) ∷ (x ≡ x : A)""#,
note "binds before ∥ are globals, after it are BVs",
testEq "refl [A] a = refl [A] a" $
equalE empty (refl (FT "A") (FT "a")) (refl (FT "A") (FT "a")),
@ -250,7 +250,7 @@ tests = "equality & subtyping" :- [
"term d-closure" :- [
testEq "★₀‹𝟎› = ★₀ : ★₁" $
equalTD 1 empty (TYPE 1) (DCloT (TYPE 0) (K Zero ::: id)) (TYPE 0),
testEq "(λᴰ i ⇒ a)‹𝟎› = (λᴰ i ⇒ a) : (a ≡ a : A)" $
testEq "(δ i ⇒ a)‹𝟎› = (δ i ⇒ a) : (a ≡ a : A)" $
equalTD 1 empty
(Eq0 (FT "A") (FT "a") (FT "a"))
(DCloT (["i"] :\\% FT "a") (K Zero ::: id))

16
tests/Tests/Typechecker.idr
View file

@ -246,7 +246,7 @@ tests = "typechecker" :- [
note "(fail) runtime-relevant type",
testTCFail "1 · A ⇏ ★₀" $
infer_ (ctx [<]) sone (F "A"),
note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ λᴰ _ ⇒ x)",
note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ δ _ ⇒ x)",
testTC "1 · refl ⇒ ⋯" $ inferAs (ctx [<]) sone (F "refl") reflTy,
testTC "1 · [refl] ⇐ ⋯" $ check_ (ctx [<]) sone (FT "refl") reflTy
],
@ -279,7 +279,7 @@ tests = "typechecker" :- [
check_ (ctx [<]) sone
(["A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0]))
reflTy,
testTC "1 · (λ A x ⇒ λᴰ i ⇒ x) ⇐ ⋯ # (def. and type of refl)" $
testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯ # (def. and type of refl)" $
check_ (ctx [<]) sone reflDef reflTy
],
@ -289,7 +289,7 @@ tests = "typechecker" :- [
testTC "x : A ⊢ 1 · (x, x) ⇐ A × A ⊳ ω·x" $
checkQ (ctx [< FT "A"]) sone
(Pair (BVT 0) (BVT 0)) (FT "A" `And` FT "A") [< Any],
testTC "1 · (a, λᴰ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $
testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $
check_ (ctx [<]) sone
(Pair (FT "a") (["i"] :\\% FT "a"))
(Sig_ "x" (FT "A") $ Eq0 (FT "A") (BVT 0) (FT "a"))
@ -360,16 +360,16 @@ tests = "typechecker" :- [
],
"equalities" :- [
testTC "1 · (λᴰ i ⇒ a) ⇐ a ≡ a" $
testTC "1 · (δ i ⇒ a) ⇐ a ≡ a" $
check_ (ctx [<]) sone (DLam $ SN $ FT "a")
(Eq0 (FT "A") (FT "a") (FT "a")),
testTC "0 · (λ p q ⇒ λᴰ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
check_ (ctx [<]) szero
(["p","q"] :\\ ["i"] :\\% BVT 1)
(Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $
Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)),
testTC "0 · (λ p q ⇒ λᴰ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
check_ (ctx [<]) szero
(["p","q"] :\\ ["i"] :\\% BVT 0)
(Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
@ -380,7 +380,7 @@ tests = "typechecker" :- [
"misc" :- [
note "0·A : Type, 0·P : A → Type, ω·p : (1·x : A) → P x",
note "⊢",
note "1 · λ x y xy ⇒ λᴰ i ⇒ p (xy i)",
note "1 · λ x y xy ⇒ δ i ⇒ p (xy i)",
note " ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i ⇒ P (xy i)] (p x) (p y)",
testTC "cong" $
check_ (ctx [<]) sone
@ -393,7 +393,7 @@ tests = "typechecker" :- [
note "0·A : Type, 0·P : ω·A → Type,",
note "ω·p q : (1·x : A) → P x",
note "⊢",
note "1 · λ eq ⇒ λᴰ i ⇒ λ x ⇒ eq x i",
note "1 · λ eq ⇒ δ i ⇒ λ x ⇒ eq x i",
note " ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q",
testTC "funext" $
check_ (ctx [<]) sone