source:
src/utilities/UnionFind.ma
@
1054
| Last change on this file since 1054 was 733, checked in by , 10 years ago | |
|---|---|
| File size: 302 bytes | |
| Line | |
|---|---|
| 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.
