Hand-computed hierarchies (checked against an independent model of the
same splitting rule). Each law is decided by normalization.
Seven roles, fan-out two: 0 -> {1, 4}; 1 -> {2, 3}; 4 -> {5, 6}.
11def binaryRootChildren :
12 (equal
13 (family StdList Nat)
14 (stdListMap
15 (family ParticipantTreeNode)
16 Nat
17 participantTreeRoleOf
18 (participantTreeChildren 2 (participantTreeNode 2 7 0)))
19 (constructor
20 StdList
21 StdListCons
22 Nat
23 1
24 (constructor StdList StdListCons Nat 4 (constructor StdList StdListEmpty Nat)))) =
25 (refl
26 (family StdList Nat)
27 (constructor
28 StdList
29 StdListCons
30 Nat
31 1
32 (constructor StdList StdListCons Nat 4 (constructor StdList StdListEmpty Nat))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.