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.
Using "Refl" as the solution for test_factorial1 (or 2) yields:
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: