source: Deliverables/D3.3/id-lookup-branch/utilities/UnionFind.ma @ 1133

Last change on this file since 1133 was 733, checked in by mulligan, 9 years ago

Fixed partial commit.

File size: 302 bytes
Line 
1include "arithmetics/nat.ma".
2
3record Info (A: Type[0]): Type[0] ≝
4{
5  UF_I_Weight: nat;
6  UF_I_Descriptor: A
7}.
8
9inductive Point (A: Type[0]): Type[0] ≝
10  UF_P_Link: Link A → Point A
11and inductive Link (A: Type[0]): Type[0] ≝
12  | UF_L_Info: Info A → Link A
13  | UF_I_Link: Point A → Link A.
Note: See TracBrowser for help on using the repository browser.