fact: Definition link t x y := let rank := rank t in let rx := get_rank x rank in let ry := get_rank y rank in let p := p t in match (compare rx ry) with | Lt => Build_UF (p [x >- y]) rank (S (size t)) | Eq => Build_UF (p [x >- y]) (rank [y >- Positive.S ry] ) (S (size t)) | Gt => Build_UF (p [y >- x]) rank (S (size t)) end .
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)