-
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.
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.