2023-05-01T08:21:12Z - 2024-05-01T08:21:12Z
Overview
9 Pull requests merged by 1 user
Merged
#43 coercion regularity
Merged
#42 check type of #[main]
Merged
#40 debug logging
Merged
#36 let
Merged
#35 allow fst, snd, case to be application heads
Merged
#29 erasure and also baby's first scheme backend
Merged
#30 #[fail]
Merged
#28 η for pairs
Merged
#19 default quantity of 1
15 Issues closed from 1 user
Closed
#24 the function part of a w value probably needs to be ω
Closed
#26 full equality check in coercion boundary
Closed
#37 check the #[main] function is the right type
Closed
#38 type checker loop in pushCoe
Closed
#34 allow "fst e"/"snd e" as an application head
Closed
#32 add pair η to Whnf.Coercion
Closed
#31 pretty printing is SLOW
Closed
#22 η for pairs
Closed
#23 make A → B a subsingleton if A is empty
Closed
#14 trim the dim context before comparing terms
Closed
#27 η for boxes
Closed
#7 crude but effective stratification
Closed
#6 default quantity
Closed
#11 coe sometimes gets stuck on a Clo
Closed
#5 file locations in errors
11 Issues created by 1 user
Opened
#9 avoid unfolding definitions in eq checking when possible
Opened
#10 quotient types
Opened
#13 do something about computeElimType
Opened
#15 there are SO MANY missing tests
Opened
#16 something for irrelevance
Opened
#17 codata
Opened
#18 implicits
Opened
#20 inductive types (W)
Opened
#21 ((((A ∷ ★⁰) ∷ ★⁰) ∷ ★⁰) ∷ ★⁰) (add a cleanup step before pretty printing)
Opened
#33 algebraic ornaments
Opened
#41 add debug logging to the rest of the compiler
3 Unresolved Conversations
Open
#4
infix operators
Open
#3
holes 🕳
Open
#1
add :pet command