Ancestors, root first: role 3 of the seven-role binary tree descends 0, 1.
103def binaryAncestors :
104 (equal
105 (family StdList Nat)
106 (stdListMap
107 (family ParticipantTreeNode)
108 Nat
109 participantTreeRoleOf
110 (participantTreeAncestors 2 7 3))
111 (constructor
112 StdList
113 StdListCons
114 Nat
115 0
116 (constructor StdList StdListCons Nat 1 (constructor StdList StdListEmpty Nat)))) =
117 (refl
118 (family StdList Nat)
119 (constructor
120 StdList
121 StdListCons
122 Nat
123 0
124 (constructor StdList StdListCons Nat 1 (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.