Representing Red-Black Trees in MetaPRL
by Alexei Kopylov
2002-2003
I'll show how we can define abstract data structures such as Set and Table in MetaPRL using depnedend records, and implement such structures using binary trees and red-black trees.
I faced some unexpected problems connecting with functionality and recursive types.
It turns out that Nuprl rules for recursive type are invalid and lead to contradiction!