| |
|
|
|
|
|
|
|
|
|
|
|
| |
Although
convenient and concise, the auto-declare behavior has on many occasions caused
confusion when a type name has accidentally been mistyped (and Dafny had then
accepted and auto-declared the name).
Note, the behavior of filling in missing type parameters is still supported. This
mode, although unusual (even original?) in languages, is different from the auto-
declare behavior. For auto-declare, identifiers could be used in the program
without having a declaration. For fill-in parameters, the implicitly declared
type parameters remain anonymous.
|
|
|
function last<T>(xs: List<T>): T
requires xs != Nil
{
match xs
case Cons(y, Nil) => y
case Cons(y, Cons(z, zs)) => last(Cons(z, zs))
}
And
function minus(x: Nat, y: Nat): Nat
{
match (x, y)
case (Zero, _) => Zero
case (Suc(_), Zero) => x
case (Suc(a), Suc(b)) => minus(a, b)
}
|
Rustan Leino