software-foundations
software-foundations copied to clipboard
testFactorial1 not solvable with "Refl"
Using "Refl" as the solution for test_factorial1 (or 2) yields:
| When checking right hand side of testFactorial1 with expected type
| factorial 3 = 6
|
| Type mismatch between
| 6 = 6 (Type of Refl)
| and
| factorial 3 = 6 (Expected type)
|
| Specifically:
| Type mismatch between
| 6
| and
| factorial 3
This is important because (1) no other tactics have been introduced at this point and (2) later in the chapter, we explicitly claim that it is solvable that way:
Now that we've defined a few datatypes and functions, let's turn to stating and proving properties of their behavior. Actually, we've already started doing this: each of the functions beginning with \idr{test} in the previous sections makes a precise claim about the behavior of some function on some particular inputs. The proofs of these claims were always the same: use \idr{Refl} to check that both sides contain identical values.
Ah, we're just missing %default total
in the header of the file, thanks.