There's a typo here, the comment here should read "return false (ff in Lean)"
def all_false : prop_var → bool
| _ := ff -- for any argument return true (tt in Lean)
This prop_eval code is a bit confusing potentially. Maybe some more explanation like this would be good
--This function takes in a proposition expression *and* a function called i representing the interpretation of all variables
def prop_eval : prop_expr → (prop_var → bool) → bool
| (var_expr v) i := i v --a variable expression evaluates to just the interpretation of that variable
| (and_expr e1 e2) i := band (prop_eval e1 i) (prop_eval e2 i) --evaluate each part of the and expression individually and then do a boolean and (band) on those values
| (or_expr e1 e2) i := bor (prop_eval e1 i) (prop_eval e2 i) --evaluate each part of the or expression individually and then do a boolean or (bor) on those values
Chapter 2.2
2.2.2
There's a typo here, the comment here should read "return false (ff in Lean)"
This
prop_eval
code is a bit confusing potentially. Maybe some more explanation like this would be good