@[irreducible]

def Paths.Building.buildPathFrom' {α : Type} (lead : MUList.State.ListToken α) (rest : MUList.State.ListST α) : Option (List Tokens.Elem.TId)

Equations

• One or more equations did not get rendered due to their size.

def Paths.Building.buildPathFrom {α : Type} (lead : Tokens.Elem.TId) (s : MUList.State.ListST α) : Option (List Tokens.Elem.TId)

Equations

• Paths.Building.buildPathFrom lead s = match Tokens.State.Tokens.get lead s with | none => none | some tkn => Paths.Building.buildPathFrom' tkn s

def Paths.Building.buildPath {α : Type} (s : MUList.State.ListST α) : Option (List Tokens.Elem.TId)

Equations

• Paths.Building.buildPath s = do let mhd ← List.head? s let hd ← mhd Paths.Building.buildPathFrom' hd s

def Paths.Building.buildFromRoot {α : Type} (rnode : Tokens.Elem.TId) (s : MUList.State.ListST α) : Option (List Tokens.Elem.TId)

Equations

• Paths.Building.buildFromRoot rnode s = if MUList.State.ListST.is_root_node rnode s = true then do let x ← Tokens.State.Tokens.get rnode s Paths.Building.buildPathFrom' x s else none