source:
src/utilities/UnionFind.ma
@
1183
| Last change on this file since 1183 was 733, checked in by , 10 years ago | |
|---|---|
| File size: 302 bytes | |
| Rev | Line | |
|---|---|---|
| [733] | 1 | include "arithmetics/nat.ma". |
| 2 | ||
| 3 | record Info (A: Type[0]): Type[0] ≝ | |
| 4 | { | |
| 5 | UF_I_Weight: nat; | |
| 6 | UF_I_Descriptor: A | |
| 7 | }. | |
| 8 | ||
| 9 | inductive Point (A: Type[0]): Type[0] ≝ | |
| 10 | UF_P_Link: Link A → Point A | |
| 11 | and 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.
