This may be a limitation or a bug either in dafny or in my understanding. Any help understanding this much appreciated.
The following dafny function verifies
datatype Tree<T> = Leaf(data: T)
| Node(left: Tree<T>, right: Tree<T>)
function treetree(t: Tree<Color>) : string
{
match t
case Leaf(_) => "zero"
case Node(Node(_,_),_) => "two"
case Node(Leaf(_),_) => "one"
}
Whereas then next function fails:
function treelist(t: Tree<List<string>>) : string
{
match t
case Leaf(Nil) => "zero"
case Leaf(Cons(_,_)) => "list"
case Node(_,_) => "two"
}
The error states that "member Leaf appears in more than one case" which I know is correct but as member Node appears in more than one case in the previous valid function I am not sure when this error actually applies.
Aucun commentaire:
Enregistrer un commentaire