Issues - rhi/quox - gec git gec git

New Issue

type checker loop in pushCoe

#38 by rhi was closed 2024-02-24 10:05:24 -05:00

check the #[main] function is the right type

#37 by rhi was closed 2024-04-14 15:15:35 -04:00

allow "fst e"/"snd e" as an application head

#34 by rhi was closed 2023-12-04 12:48:43 -05:00

add pair η to Whnf.Coercion

#32 by rhi was closed 2023-11-03 13:15:31 -04:00

pretty printing is SLOW

#31 by rhi was closed 2023-10-25 15:07:38 -04:00

η for boxes

#27 by rhi was closed 2023-09-17 13:11:27 -04:00

full equality check in coercion boundary

#26 by rhi was closed 2024-04-18 16:18:20 -04:00

the function part of a w value probably needs to be ω

#24 by rhi was closed 2024-04-20 21:45:15 -04:00

make A → B a subsingleton if A is empty

#23 by rhi was closed 2023-09-17 14:11:44 -04:00

η for pairs

#22 by rhi was closed 2023-09-19 17:22:34 -04:00

trim the dim context before comparing terms

#14 by rhi was closed 2023-09-17 13:20:13 -04:00

coe sometimes gets stuck on a Clo

#11 by rhi was closed 2023-07-16 21:50:57 -04:00

fix the parser to produce actual errors

#8 by rhi was closed 2023-04-24 22:56:21 -04:00

crude but effective stratification

#7 by rhi was closed 2023-07-22 15:28:02 -04:00

default quantity

#6 by rhi was closed 2023-07-21 11:58:19 -04:00

file locations in errors

#5 by rhi was closed 2023-05-21 14:38:02 -04:00

add multi-name binders like 0.(m n ℕ) → ⋯

#2 by rhi was closed 2023-04-19 15:38:07 -04:00