-
Notifications
You must be signed in to change notification settings - Fork 0
Spring 2022
Mondays @ 2:00–3:00pm in Olek's Zoom
We are continuing through PLFA. Similar to last semester, we will aim to alternate weeks between interactively reading through a chapter and doing exercises. We hope to have a leader for each exercise session to run through the problems.
- "C-c C-." - "agda2-goal-and-context-and-inferred": Goal type, context and inferred type
- "M-." - "agda2-goto-definition-keyboard": Go to definition of identifier under point
- "C-x C-u =" - "describe-char": put your cursor on a symbol to get information about it
Attendees: Olek, Artem, John Li, Andrew
Summary: We finished reading Isomorphism, and the binary exercise (which was just copy and pasting from Induction and then constructing the record). Next time we will read Connectives. We read just the few first sentences, and discussed how you can nest and partially apply the tuple constructor.
Homework: None for this week!
Attendees: Olek, Artem, John Li, Matt
Summary: We finished reading Equality, and started reading Isomorphism up through Isomorphism. Next time we will continue reading with Isomorphism as an equivalence.
Homework: None for this week!
Attendees: Olek, Artem, John Li, Matt
Summary: We continued reading Equality, and got hung up on Rewriting Expanded. We spent a while examining how the multi pattern match worked. We spent part of the time reading through the McBride 2004 paper to see how with abstractions worked, and found the examples on page 20 somewhat informative. We also played around with some minimal examples, and found that the strategy for desugaring a with clause into a where defined helper function had some heuristics for argument ordering that weren't necessarily easy to follow. We failed to break these heuristics and convinced ourselves it would be hard to, assuming our understanding of how they work is correct!
Homework: None for this week!
Attendees: Olek, Artem, John Li, Matt
Summary: We started reading Equality, and got up to Multiple Rewrites.
Homework: Do <=-Reasoning if you're feeling particularly motivated.
Attendees: Olek, Artem, John Li
Summary: We worked through the trichotomy and o+o=e, exercises. We notably spent some time thinking about how to search for definitions, and found C-c C-z to be helpful for that. Next time, we will start reading Equality
Homework: Do the o+o=e and Bin-predicates exercises.
Attendees: Olek, Julia, Artem, John Li, Andrew
Summary: We worked through the *-mono-<=, <-trans, <=-iff-<, and <-trans-revisited exercises. Next time, we will go over the remaining homework and start reading Equality
Homework: Do the trichotomy and Bin-predicates exercises.
Attendees: Olek, Artem, Julia, John Li
Summary: We continued reading Relations up through the section Monotonicity.
Homework: Do the *-mono-<= exercise, and if you can, read through strict inequality and do the exercises there.
Attendees: Olek, Artem, Julia, John Li, Andrew
Summary: We read Relations up through the section Reflexivity, and collaboratively did the orderings exercise.
Homework: Review an exercise in Induction to refamiliarize yourself with keybindings. Naturals has a short list of useful keybindings, and the agda-mode doc has a much more in depth list.