search

kevinsullivan / cs6501s23

Formal Mathematics for Software Design
6 stars 6 forks source link

2.2.2. Semantics - Typo #25

Open sm4sa opened 1 year ago

sm4sa commented 1 year ago

"def all_false : propvar → bool | := ff -- for any argument return true (tt in Lean)"

I believe the comment should be, "for any argument return false (ff in Lean)"

sm4sa commented 1 year ago

"So we now have is a specification of the syntax and semantics of a subset of propositional logic. "

I believe "So what we now have is a specification of the syntax and semantics of a subset of propositional logic. " works better

sm4sa commented 1 year ago

The examples throughout 2.2.2. for the most part made sense to me, besides small pieces of lean syntax unfamiliar to me. However, the def prop_eval example seemed like a bit of a jump in difficulty. I would almost recommend making the def prop_eval part into an exercise for students to try as a small in-class exercise by giving them bits of pieces of the code as skeleton code and having students fill out the rest, using test cases to make sure they got it correct. Then, doing prop_eval for the in-class exercise operators should be easier for students to figure out on their own.