4.2.2. Operations:
"When proving function or other data type, however, the particular value of the type that you construct is usually important. "
I believe it should be something like "When proving a function or another data type, however, the particular value of the type that you construct is usually important. "
4.3.1. Data Type
"The list data type is surprising similar to the nat data type. Where as a larger nat is constructed from only a smaller nat, a larger list is constructed from a new first element (the head of the new list) and a smaller list (the tail of the new list)."
Should be "The list data type is surprisingly similar to the nat data type. Whereas a larger nat is constructed from only a smaller nat, a larger list is constructed from a new first element (the head of the new list) and a smaller list (the tail of the new list)."
4.3.4. Partial Functions
"Let’s see some fo the solutions that are available."
Should be "Let’s see some of the solutions that are available."
4.3.4.2. Option values
"The next solution changes the type of the function, so that return value is in the form of a variant type, a value of which is either none or some valid return value."
Should be something like "The next solution changes the type of the function, so that the return value is in the form of a variant type, a value of which is either none or some valid return value."
4.3.4.3. Precondition
"Let’s see how e might first write the function using a tactic script, to take advantage of your familiarity with using it to build proofs."
Should be "Let’s see how be might first write the function using a tactic script, to take advantage of your familiarity with using it to build proofs."
4.4.3. Map
"Of course well run into exactly the same sort of problem, of having to engage in error-prone cloning and editing of code, if we want to now map lists of Boolean values to lists of strings (e.g., mapping each tt to “T” and each ff to “F”).
And you can imagine many other examples: mapping lists of employees to list of their corresponding salaries, or mapping lists of Boolean values to lists of their negations, etc. "
Should be "Of course we'll run into exactly the same sort of problem, of having to engage in error-prone cloning and editing of code, if we want to now map lists of Boolean values to lists of strings (e.g., mapping each tt to “T” and each ff to “F”).
And you can imagine many other examples: mapping lists of employees to lists of their corresponding salaries, or mapping lists of Boolean values to lists of their negations, etc.
"
"The answer should now we pretty clear:"
Should be "The answer should now be pretty clear:"
4.5. Recursive Proofs
"provide a concrete and pecific example of this reasoning and how we can automate it using tools we already have, concluding what is called the induction axiom for natural numbers (arguments to P);"
Should be "provide a concrete and specific example of this reasoning and how we can automate it using tools we already have, concluding what is called the induction axiom for natural numbers (arguments to P);"
4.5.1. The Idea by Example
"The simp tactict tries to find, and if found applies, rules/axioms from the definition of the listed functions: here from just nat.add."
Should be "The simp tactic tries to find, and if found applies, rules/axioms from the definition of the listed functions: here from just nat.add."
4.5.1.2. A Solution
"From a proof that 0 is a left identity for 0 can we build a proof that 0 is a left identity for one!"
Should be "From a proof that 0 is a left identity for 0 we can build a proof that 0 is a left identity for one!"
4.5.1.8. Monoids and Foldr
"We can now define a general structure that we can instantiate to formally represent either and additive or a multiplicative monoid on the natural numbers."
Should be "We can now define a general structure that we can instantiate to formally represent either an additive or a multiplicative monoid on the natural numbers."
4.5.2.2. Induction Axiom for Lists
"We see again that there’s nothing myseterious about proof by induction."
Should be "We see again that there’s nothing mysterious about proof by induction."
"Every inductive axiom can be understood as a proof of universal generalization that asserts that every value of some input type has a corresponging result value of type."
Should be "Every inductive axiom can be understood as a proof of universal generalization that asserts that every value of some input type has a corresponding result value of type."
4.2.2. Operations: "When proving function or other data type, however, the particular value of the type that you construct is usually important. " I believe it should be something like "When proving a function or another data type, however, the particular value of the type that you construct is usually important. "
4.3.1. Data Type "The list data type is surprising similar to the nat data type. Where as a larger nat is constructed from only a smaller nat, a larger list is constructed from a new first element (the head of the new list) and a smaller list (the tail of the new list)." Should be "The list data type is surprisingly similar to the nat data type. Whereas a larger nat is constructed from only a smaller nat, a larger list is constructed from a new first element (the head of the new list) and a smaller list (the tail of the new list)."
4.3.4. Partial Functions "Let’s see some fo the solutions that are available." Should be "Let’s see some of the solutions that are available."
4.3.4.2. Option values "The next solution changes the type of the function, so that return value is in the form of a variant type, a value of which is either none or some valid return value." Should be something like "The next solution changes the type of the function, so that the return value is in the form of a variant type, a value of which is either none or some valid return value."
4.3.4.3. Precondition "Let’s see how e might first write the function using a tactic script, to take advantage of your familiarity with using it to build proofs." Should be "Let’s see how be might first write the function using a tactic script, to take advantage of your familiarity with using it to build proofs."
4.4.3. Map "Of course well run into exactly the same sort of problem, of having to engage in error-prone cloning and editing of code, if we want to now map lists of Boolean values to lists of strings (e.g., mapping each tt to “T” and each ff to “F”). And you can imagine many other examples: mapping lists of employees to list of their corresponding salaries, or mapping lists of Boolean values to lists of their negations, etc. " Should be "Of course we'll run into exactly the same sort of problem, of having to engage in error-prone cloning and editing of code, if we want to now map lists of Boolean values to lists of strings (e.g., mapping each tt to “T” and each ff to “F”). And you can imagine many other examples: mapping lists of employees to lists of their corresponding salaries, or mapping lists of Boolean values to lists of their negations, etc. "
"The answer should now we pretty clear:" Should be "The answer should now be pretty clear:"
4.5. Recursive Proofs "provide a concrete and pecific example of this reasoning and how we can automate it using tools we already have, concluding what is called the induction axiom for natural numbers (arguments to P);" Should be "provide a concrete and specific example of this reasoning and how we can automate it using tools we already have, concluding what is called the induction axiom for natural numbers (arguments to P);"
4.5.1. The Idea by Example "The simp tactict tries to find, and if found applies, rules/axioms from the definition of the listed functions: here from just nat.add." Should be "The simp tactic tries to find, and if found applies, rules/axioms from the definition of the listed functions: here from just nat.add."
4.5.1.2. A Solution "From a proof that 0 is a left identity for 0 can we build a proof that 0 is a left identity for one!" Should be "From a proof that 0 is a left identity for 0 we can build a proof that 0 is a left identity for one!"
4.5.1.8. Monoids and Foldr "We can now define a general structure that we can instantiate to formally represent either and additive or a multiplicative monoid on the natural numbers." Should be "We can now define a general structure that we can instantiate to formally represent either an additive or a multiplicative monoid on the natural numbers."
4.5.2.2. Induction Axiom for Lists "We see again that there’s nothing myseterious about proof by induction." Should be "We see again that there’s nothing mysterious about proof by induction."
"Every inductive axiom can be understood as a proof of universal generalization that asserts that every value of some input type has a corresponging result value of type." Should be "Every inductive axiom can be understood as a proof of universal generalization that asserts that every value of some input type has a corresponding result value of type."