Commit b68e35e5 authored by Mario Pereira's avatar Mario Pereira
Browse files

New theories tree.Tree and tree.Size

parent bfc08a83
theory Tree
use import list.List
type forest 'a = list (tree 'a)
with tree 'a = Node 'a (forest 'a)
end
theory Size
use import Tree
use import list.List
use import int.Int
let rec function size_forest (f: forest 'a) : int
ensures { result >= 0 }
= match f with
| Nil -> 0
| Cons t f -> size_tree t + size_forest f
end
with function size_tree (t: tree 'a) : int
ensures { result > 0 }
= match t with
| Node _ f -> 1 + size_forest f
end
end
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment