{"items":[{"id":"bb9ab6ca-5fc5-4604-9bb5-24edf0f93174","type":"push","org":"zhengqunkoo","repo":"YSC3236","title":"Add mystery functions definitions to week 5 materials","summary":"This commit adds a suite of 'mystery function' specifications—ranging from standard mathematical functions like factorial and Fibonacci to more abstract tree transformations—to the week-05 course exercises. These definitions serve as formal specification exercises for students in the Functional Programming in Proof (FPP) curriculum.","url":"https://nomit.dev/zhengqunkoo/YSC3236/status/2c945403208a6e7f577c3ed2b0af2a3e5c15b42caed79974bb3d9294e5af0b1c","author":"xsot","contributors":["xsot"],"updated_at":"2020-09-12T13:49:32+00:00"},{"id":"24a49df0-5bbd-4a3d-976a-2d322a532352","type":"push","org":"zhengqunkoo","repo":"YSC3236","title":"Add the week 5 Coq mystery-functions exercise file to provide formal specifications and proof scaffolding for functional programming practice.","summary":"This commit introduces a substantial Coq worksheet centered on “mystery functions,” with formal specifications over naturals, booleans, tuples, and trees, plus example implementations and partial proof scripts. It looks like teaching or lab material: students are guided to identify functions from algebraic properties, write unit tests, and prove soundness or uniqueness where possible. The file adds real instructional content rather than boilerplate, and it expands the project with a reusable set of proof exercises and examples. Practically, it gives contributors a new verified-programming exercise set to work through.","url":"https://nomit.dev/zhengqunkoo/YSC3236/status/01be7490873cad4b6bdbfc038483b14ff4094c02ee4e11641f2db9920ac5f0f3","author":"","contributors":[],"updated_at":"2020-09-12T08:04:03+00:00"},{"id":"5e0818e6-a353-4e99-9265-225f27528e2e","type":"push","org":"zhengqunkoo","repo":"YSC3236","title":"Updated exercise 13 in the backward/forward proofs notes to swap the proof strategies and make the proof-term growth tradeoffs explicit.","summary":"This commit rewrites the Coq solutions for `ladidah` and `toodeloo` so they now use the opposite proof styles: `ladidah` is proved by destructing the disjunction early and replaying the implication chain in each branch, while `toodeloo` is proved by splitting early and rebuilding the same derivation for each conjunct. The surrounding commentary and shown proof terms were updated to match, with the notes now emphasizing how early `destruct`/`split` affects duplication and proof size. Practically, this makes exercise 13 a clearer comparison of forward vs. backward proof structure and their linear proof-term complexity.","url":"https://nomit.dev/zhengqunkoo/YSC3236/status/42b8138bf05e2f4be83871852496db7347d27d2262cf20a83b16b52d151c3b92","author":"","contributors":[],"updated_at":"2020-09-11T13:43:00+00:00"},{"id":"f7db4cc9-3e9f-4ce5-afaf-35ad4211d13c","type":"push","org":"zhengqunkoo","repo":"YSC3236","title":"Completed the write-up for Exercise 12c by documenting the proof comparison in week 4's backward-and-forward proofs notes.","summary":"This change finishes the pending 12c section in the Coq exercise file by replacing the TODO with an explicit comparison between the two existing proof styles. The added note highlights that one proof repeatedly reconstructs the same implication chain while the other avoids that redundancy, which clarifies the tradeoff the exercise is meant to illustrate. Practically, the file is now more complete as study material and makes the proof-structure lesson easier to understand.","url":"https://nomit.dev/zhengqunkoo/YSC3236/status/14f18205b43ec122dd6dab3a1753cf5db3f7a53fbf8a245355fbff711c4ee357","author":"","contributors":[],"updated_at":"2020-09-10T23:13:44+00:00"},{"id":"8d856629-91fc-4cf5-994b-598a55192dd2","type":"push","org":"zhengqunkoo","repo":"YSC3236","title":"Hide supporting proof material and label multiplication exercises to make the week 4 Coq worksheet easier to navigate.","summary":"This change reorganizes `week-04_backward-and-forward-proofs.v` for readers rather than altering the underlying proofs or definitions. It wraps auxiliary sections in hide markers and adds explicit exercise labels for the multiplication tasks, which should make the rendered material cleaner and easier for students to follow. The practical effect is better structure and readability in the teaching content, with no semantic change to the Coq development.","url":"https://nomit.dev/zhengqunkoo/YSC3236/status/72d6512a682948728255858126a668ea7753b5b655d40f82e8421c2f9cf6f083","author":"","contributors":[],"updated_at":"2020-09-09T11:57:53+00:00"}],"pagination":{"offset":0,"limit":5,"has_more":true}}