Use more original-agda-like notation, and add more solutions - #22

Open

srghma wants to merge 12 commits into

rami3l:masterfrom

srghma:feat_better_arrows

Commits on Aug 8, 2026

feat: use ⇒ instead of : to match agda book more
srghma
committed
e592f62
feat: Lambda -> impelement primed excercise
srghma
committed
dfc6b08
refactor: Lambda -> add newlines for cases to match agda more
srghma
committed
7245a7f
feat: add solution for Lambda/#exercise-_-stretch
srghma
committed
0dcfeff
docs: improve comment
srghma
committed
4bee86f
fix: rebase mistake, make lake build pass
srghma
committed
54f2400
feat: make Reduce be defined more similar to the book by using non-hygenic notation
srghma
committed
279fcac
feat: prove that Clos and Clos` are not iso
srghma
committed
ecec4dd
feat: make Reduce be defined more similar to the book by using non-hygenic notation
srghma
committed
05ba26f
fix: deelab
srghma
committed
50a105d
feat: explain the need for `x ≠ y` in `Lookup`
srghma
committed
19881aa

Commits on Aug 9, 2026

feat: add more comments explaining why
srghma
committed
97bf753