rhi
0 Followers · 0 Following
  • Joined on 2020-06-10
Repositories
22
 Projects Packages Public Activity Starred Repositories
rhi deleted branch reg from rhi/quox 2024-04-18 16:18:20 -04:00
rhi pushed to 🐉 at rhi/quox 2024-04-18 16:18:20 -04:00
c9f66bb6af minor refactor
7f72ed56fb add test for regularity
67c825ab39 add coercion regularity to the equality checker (not to whnf)
ddc2422ffb fix .gitignore
Compare 4 commits »
rhi closed issue rhi/quox#26 2024-04-18 16:18:20 -04:00
full equality check in coercion boundary
rhi merged pull request rhi/quox#43 2024-04-18 16:18:20 -04:00
coercion regularity
rhi pushed to reg at rhi/quox 2024-04-18 05:49:23 -04:00
c9f66bb6af minor refactor
rhi pushed to reg at rhi/quox 2024-04-15 16:58:36 -04:00
7f72ed56fb add test for regularity
67c825ab39 add coercion regularity to the equality checker (not to whnf)
Compare 2 commits »
rhi pushed to 🐉 at rhi/quox 2024-04-15 16:41:44 -04:00
3f7031c613 pack bump
rhi created pull request rhi/quox#43 2024-04-15 16:41:32 -04:00
coercion regularity
rhi pushed to reg at rhi/quox 2024-04-15 16:41:11 -04:00
9a92ea5463 add test for regularity
92ac4a0d05 add coercion regularity directly
ddc2422ffb fix .gitignore
3f7031c613 pack bump
Compare 4 commits »
rhi created branch reg in rhi/quox 2024-04-15 16:41:11 -04:00
rhi commented on issue rhi/quox#26 2024-04-14 16:09:29 -04:00
full equality check in coercion boundary

test case:

def0 ugh : (A : ★) → (AA : A ≡ A : ★) → (s : A) →
           (P : A → ★) → P s → P (coe (𝑖 ⇒ AA @𝑖) s) =
  λ A AA s P p ⇒ p
rhi commented on issue rhi/quox#26 2024-04-14 15:35:18 -04:00
full equality check in coercion boundary

the rule in xtt (coercion regularity):


\frac{
  \Psi, j, j' \mid \Gamma \vdash
    A\langle j/i \rangle = A\langle j'/i \rangle \; \mathit{type}_k
}{
  \Psi \mid \Gamma \vdash
   …
rhi deleted branch maincheck from rhi/quox 2024-04-14 15:15:36 -04:00
rhi pushed to 🐉 at rhi/quox 2024-04-14 15:15:36 -04:00
8823154973 add golden test stuff
b7dc5ffdc4 add check for #[main] type
dd697ba56e add CheckBuiltin
32b9fe124f minor tweaks in Q.Typing.Context
Compare 4 commits »
rhi closed issue rhi/quox#37 2024-04-14 15:15:35 -04:00
check the #[main] function is the right type
rhi merged pull request rhi/quox#42 2024-04-14 15:15:35 -04:00
check type of #[main]
rhi pushed to maincheck at rhi/quox 2024-04-14 14:50:06 -04:00
8823154973 add golden test stuff
rhi created pull request rhi/quox#42 2024-04-14 10:21:06 -04:00
check type of #[main]
rhi pushed to maincheck at rhi/quox 2024-04-14 10:20:56 -04:00
b7dc5ffdc4 add check for #[main] type
dd697ba56e add CheckBuiltin
32b9fe124f minor tweaks in Q.Typing.Context
Compare 3 commits »
rhi created branch maincheck in rhi/quox 2024-04-14 10:20:56 -04:00